Logic for Computer Scientists/Propositional Logic/Horn clauses

From Wikibooks, the open-content textbooks collection

Jump to: navigation, search

Contents

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

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

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

[edit] Problems

[edit] Problem 20 (Propositional)

Let F be a propositional logical formulae and S a subset atomic formula occurring in F. Let TS(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 TS(F) is equivalent to a Horn formula H (i.e. T_S(F) \equiv H).

\Box

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

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

Retrieved from "http://en.wikibooks.org/wiki/Logic_for_Computer_Scientists/Propositional_Logic/Horn_clauses"