Logic for Computer Scientists/Propositional Logic/Horn clauses

Horn clauses

In this subsection we introduce a special class of formulae which are of particular interest for logic programming. Furthermore it turns out that these formulae admit an efficient test for satisfiability.

Definition 9

A formula is a Horn formula if it is in CNF and every disjunction contains at most one positive literal. Horn clauses are clauses, which contain at most one positive literal.

$F = (A \lor \lnot B)$       $\land$   $(\lnot C \lor \lnot A \lor D)$

$\land (\lnot A \lor \lnot B)$       $\land$   $D \land \lnot E$

$F \equiv (B \to A)$            $\land$   $(C \land A \to D)$

$\land (A \land B \to false)$    $\land$   $(true \to D)\land (E \to false)$

where $true$ is a tautology and $false$ is an unsatisfiable formula.

In clause form this can be written as

$\{\{ A,\lnot B\}, \{ \lnot C, \lnot A, D\} , \{\lnot A, \lnot B \} , \{ D \}, \{ \lnot E\}\}$

and in the context of logic programming this is written as:

$\{ A \gets B$

  $D \gets A,C$

$\gets A, B$

$\gets E$

   $D \gets$      $\}$

For Horn formula there is an efficient algorithm to test satisfiability of a formula $F$ :

Deciding Satisfiability of Horn Formulae If there is a subformula of the kind $true \to A$ label every occurrence of $A$ in $F$. Apply the following rules until none of them is applicable: If $A_1 \land \cdots \land A_n \to B$ is a subformula and $A_1 \cdots A_n$ are all labeled and $B$ is not labeled then label every occurrence of $B$ in $F$. If $A_1 \land \cdots \land A_n \to false$ is a subformula and $A_1 \cdots A_n$ are all labeled then Stop: Unsatisfiable Stop: Satisfiable The assignment $\mathcal{A}(A) = true$ iff $A$ is labeled is a model.

Theorem 6

The above algorithm is correct and stops after $n$ steps, where $n$ is the number of atoms in the formula.

As an immediate consequence we see, that a Horn formula is satisfiable if there is no subformula of the form $A_1 \land \cdots \land A_n \to false$.

Horn formulae admit unique least models, i.e. $\mathcal{A}$ is a unique least model for $F$ if for every model $\mathcal{A}'$ and for every atom B in F holds: if $\mathcal{A}(B) = true$ then $\mathcal{A}'(B) = true$ . Note, that this unique least model property does not hold for non Horn formulae: as an example take $A \lor B$ which is obviously non Horn. $\mathcal{A}_1(A) = true, \mathcal{A}_1(B) = false$ is a least model and $\mathcal{A}_2(A) = false, \mathcal{A}_2(B) = true$ as well, hence we have two least models.

Problems

Problem 20 (Propositional)

Let $F$ be a propositional logical formulae and $S$ a subset atomic formula occurring in $F$. Let $T_S(F)$ be the formula which results from $F$ by replacing all occurrences of an atomic formulae $A \in S$ by $\lnot A$. Example: $T_{\{A\}}(A \land B) = \lnot A \land B$. Prove or disprove: There exists an $S$ for

1. $F = A \stackrel{\cdot} \vee B$ or
2. $F = A \stackrel{\cdot} \vee B \stackrel{\cdot} \vee C$, so that $T_S(F)$ is equivalent to a Horn formula $H$ (i.e. $T_S(F) \equiv H$).
   

$\Box$

Problem 21 (Propositional)

Apply the marking algorithm to the following formula F.

Which is a least model?

$(A \lor \lnot D \lor \lnot E) \land (B \lor \lnot C) \land (\lnot B \lor \lnot D) \land D \land (\lnot D \lor E)$

1. $F = (\lnot A \lor \lnot B \lor \lnot C) \land \lnot D \land(\lnot E \lor A) \land E \land B \land (\lnot F \lor C) \land F$
2. $F = (A \lor \lnot D \lor \lnot E) \land (B \lor \lnot C) \land (\lnot B \lor \lnot D) \land D \land (\lnot D \lor E)$

$\Box$

Problem 22 (Propositional)

Decide which one of the indicated CNFs are Horn formulae and transform then into a conjunction of implications:

1. $(A \lor B \lor C) \land (A \lor \lnot C) \land (\lnot A \lor B) \land \lnot B$
2. $(S \lor \lnot P \lor Q) \land (S \lor \lnot P \lor \lnot R)$
3. $(A \lor \lnot A)$
4. $A \land (\lnot A \lor B) \land (\lnot B \lor \lnot C \lor D) \land (\lnot E) \land (\lnot A \lor \lnot C) \land D$

$\Box$