Logic for Computer Scientists/Propositional Logic/Horn clauses

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Propositional Logic
Jump to: navigation, search

Horn clauses[edit]

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[edit]

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[edit]

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[edit]

Problem 20 (Propositional)[edit]

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)[edit]

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)[edit]

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