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$ 