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\vee \mathrm{\neg }B)$       $\wedge$   $(\mathrm{\neg }C\vee \mathrm{\neg }A\vee D)$

$\wedge (\mathrm{\neg }A\vee \mathrm{\neg }B)$       $\wedge$   $D\wedge \mathrm{\neg }E$

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

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

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

In clause form this can be written as

$\{\{A,\mathrm{\neg }B\},\{\mathrm{\neg }C,\mathrm{\neg }A,D\},\{\mathrm{\neg }A,\mathrm{\neg }B\},\{D\},\{\mathrm{\neg }E\}\}$

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

$\{A\leftarrow B$

  $D\leftarrow A,C$

$\leftarrow A,B$

$\leftarrow E$

   $D\leftarrow$      $\}$

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

Template:Box

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\wedge \cdots \wedge A_n\to false$.

Horn formulae admit unique least models, i.e. $𝒜$ is a unique least model for $F$ if for every model ${𝒜}^{\prime }$ and for every atom B in F holds: if $𝒜(B)=true$ then ${𝒜}^{\prime }(B)=true$ . Note, that this unique least model property does not hold for non Horn formulae: as an example take $A\vee B$ which is obviously non Horn. ${𝒜}_1(A)=true,{𝒜}_1(B)=false$ is a least model and ${𝒜}_2(A)=false,{𝒜}_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 $\mathrm{\neg }A$. Example: $T_{\{A\}}(A\wedge B)=\mathrm{\neg }A\wedge 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$).
   

$◻$

Problem 21 (Propositional)

Apply the marking algorithm to the following formula F.

Which is a least model?

$(A\vee \mathrm{\neg }D\vee \mathrm{\neg }E)\wedge (B\vee \mathrm{\neg }C)\wedge (\mathrm{\neg }B\vee \mathrm{\neg }D)\wedge D\wedge (\mathrm{\neg }D\vee E)$

1. $F=(\mathrm{\neg }A\vee \mathrm{\neg }B\vee \mathrm{\neg }C)\wedge \mathrm{\neg }D\wedge (\mathrm{\neg }E\vee A)\wedge E\wedge B\wedge (\mathrm{\neg }F\vee C)\wedge F$
2. $F=(A\vee \mathrm{\neg }D\vee \mathrm{\neg }E)\wedge (B\vee \mathrm{\neg }C)\wedge (\mathrm{\neg }B\vee \mathrm{\neg }D)\wedge D\wedge (\mathrm{\neg }D\vee E)$

$◻$

Problem 22 (Propositional)

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

1. $(A\vee B\vee C)\wedge (A\vee \mathrm{\neg }C)\wedge (\mathrm{\neg }A\vee B)\wedge \mathrm{\neg }B$
2. $(S\vee \mathrm{\neg }P\vee Q)\wedge (S\vee \mathrm{\neg }P\vee \mathrm{\neg }R)$
3. $(A\vee \mathrm{\neg }A)$
4. $A\wedge (\mathrm{\neg }A\vee B)\wedge (\mathrm{\neg }B\vee \mathrm{\neg }C\vee D)\wedge (\mathrm{\neg }E)\wedge (\mathrm{\neg }A\vee \mathrm{\neg }C)\wedge D$

$◻$