# Logic for Computer Scientists/Propositional Logic/Horn clauses

## Horn clausesEdit

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 9Edit

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 If there is a subformula of the kind ${\displaystyle true\to A}$  label every occurrence of ${\displaystyle A}$  in ${\displaystyle F}$ . 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 Stop: Satisfiable The assignment ${\displaystyle {\mathcal {A}}(A)=true}$  iff ${\displaystyle A}$  is labeled is a model.

## Theorem 6Edit

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.

## ProblemsEdit

#### Problem 20 (Propositional)Edit

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)Edit

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)Edit

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 }$