# 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.

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

${\displaystyle \land (\lnot A\lor \lnot B)}$       ${\displaystyle \land }$   ${\displaystyle D\land \lnot E}$

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

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

where ${\displaystyle true}$ is a tautology and ${\displaystyle false}$ is an unsatisfiable formula.

In clause form this can be written as

${\displaystyle \{\{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:

${\displaystyle \{A\gets B}$

${\displaystyle D\gets A,C}$
${\displaystyle \gets A,B}$
${\displaystyle \gets E}$

${\displaystyle D\gets }$      ${\displaystyle \}}$

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

Deciding Satisfiability of Horn Formulae

1. If there is a subformula of the kind ${\displaystyle true\to A}$ label every occurrence of ${\displaystyle A}$ in ${\displaystyle F}$.
2. Apply the following rules until none of them is applicable:
• If ${\displaystyle A_{1}\land \cdots \land A_{n}\to B}$ is a subformula and ${\displaystyle A_{1}\cdots A_{n}}$ are all labeled and ${\displaystyle B}$ is not labeled then label every occurrence of ${\displaystyle B}$ in ${\displaystyle F}$.
• If ${\displaystyle A_{1}\land \cdots \land A_{n}\to false}$ is a subformula and ${\displaystyle A_{1}\cdots A_{n}}$ are all labeled then Stop: Unsatisfiable
3. Stop: Satisfiable The assignment ${\displaystyle {\mathcal {A}}(A)=true}$ iff ${\displaystyle A}$ is labeled is a model.

## Theorem 6

The above algorithm is correct and stops after ${\displaystyle n}$ steps, where ${\displaystyle 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 ${\displaystyle A_{1}\land \cdots \land A_{n}\to false}$.

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

## Problems

#### Problem 20 (Propositional)

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

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

${\displaystyle \Box }$

#### Problem 21 (Propositional)

Apply the marking algorithm to the following formula F.

Which is a least model?

${\displaystyle (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. ${\displaystyle 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. ${\displaystyle 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)}$

${\displaystyle \Box }$

#### Problem 22 (Propositional)

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

1. ${\displaystyle (A\lor B\lor C)\land (A\lor \lnot C)\land (\lnot A\lor B)\land \lnot B}$
2. ${\displaystyle (S\lor \lnot P\lor Q)\land (S\lor \lnot P\lor \lnot R)}$
3. ${\displaystyle (A\lor \lnot A)}$
4. ${\displaystyle 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}$

${\displaystyle \Box }$