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.

         

         

               

       

where is a tautology and is an unsatisfiable formula.

In clause form this can be written as

and in the context of logic programming this is written as:


  


         


For Horn formula there is an efficient algorithm to test satisfiability of a formula  :



Deciding Satisfiability of Horn Formulae


  1. If there is a subformula of the kind label every occurrence of in .
  2. Apply the following rules until none of them is applicable:
    • If is a subformula and are all labeled and is not labeled then label every occurrence of in .
    • If is a subformula and are all labeled then Stop: Unsatisfiable
  3. Stop: Satisfiable The assignment iff is labeled is a model.

Theorem 6[edit]

The above algorithm is correct and stops after steps, where 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 .

Horn formulae admit unique least models, i.e. is a unique least model for if for every model and for every atom B in F holds: if then . Note, that this unique least model property does not hold for non Horn formulae: as an example take which is obviously non Horn. is a least model and as well, hence we have two least models.

Problems[edit]

Problem 20 (Propositional)[edit]

Let be a propositional logical formulae and a subset atomic formula occurring in . Let be the formula which results from by replacing all occurrences of an atomic formulae by . Example: . Prove or disprove: There exists an for

  1. or
  2. , so that is equivalent to a Horn formula (i.e. ).

Problem 21 (Propositional)[edit]

Apply the marking algorithm to the following formula F.

Which is a least model?




Problem 22 (Propositional)[edit]

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