Logic for Computer Scientists/Propositional Logic/Horn clauses

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?

 


  1.  
  2.  



 

Problem 22 (Propositional) edit

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

  1.  
  2.  
  3.  
  4.