# 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$ :
* 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
* $F=A{\stackrel {\cdot }{\vee }}B$ or
* $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)$
* $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$
* $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:
* $(A\lor B\lor C)\land (A\lor \lnot C)\land (\lnot A\lor B)\land \lnot B$
* $(S\lor \lnot P\lor Q)\land (S\lor \lnot P\lor \lnot R)$
* $(A\lor \lnot A)$
* $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$