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

1. If there is a subformula of the kind $true\to A$ label every occurrence of $A$ in $F$.
   
2. 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
     

3. 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$