Logic for Computer Scientists/Propositional Logic/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.

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.

where t r u e is a tautology and f a l s e 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 F :

1. If there is a subformula of the kind t r u e → A label every occurrence of A in F .
   
2. Apply the following rules until none of them is applicable:
   
   • If A 1 ∧ ⋯ ∧ A n → B \land \cdots \land A_\to B> is a subformula and A 1 ⋯ A n \cdots A_> are all labeled and B is not labeled then label every occurrence of B in F .
     
   • If A 1 ∧ ⋯ ∧ A n → f a l s e \land \cdots \land A_\to false> is a subformula and A 1 ⋯ A n \cdots A_> are all labeled then Stop: Unsatisfiable
     
3. Stop: Satisfiable The assignment A ( A ) = t r u e (A)=true> iff A is labeled is a model.
   

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 ∧ ⋯ ∧ A n → f a l s e \land \cdots \land A_\to false> .

Problems

Problem 20 (Propositional)

Let F be a propositional logical formulae and S a subset atomic formula occurring in F . Let T S ( F ) (F)> be the formula which results from F by replacing all occurrences of an atomic formulae A ∈ S by ¬ A . Example: T < A >( A ∧ B ) = ¬ A ∧ B >(A\land B)=\lnot A\land B> . Prove or disprove: There exists an S for

Problem 21 (Propositional)

Apply the marking algorithm to the following formula F.

Which is a least model?

( A ∨ ¬ D ∨ ¬ E ) ∧ ( B ∨ ¬ C ) ∧ ( ¬ B ∨ ¬ D ) ∧ D ∧ ( ¬ D ∨ E )

1. F = ( ¬ A ∨ ¬ B ∨ ¬ C ) ∧ ¬ D ∧ ( ¬ E ∨ A ) ∧ E ∧ B ∧ ( ¬ F ∨ C ) ∧ F
2. F = ( A ∨ ¬ D ∨ ¬ E ) ∧ ( B ∨ ¬ C ) ∧ ( ¬ B ∨ ¬ D ) ∧ D ∧ ( ¬ D ∨ E )

Problem 22 (Propositional)

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

1. ( A ∨ B ∨ C ) ∧ ( A ∨ ¬ C ) ∧ ( ¬ A ∨ B ) ∧ ¬ B
2. ( S ∨ ¬ P ∨ Q ) ∧ ( S ∨ ¬ P ∨ ¬ R )
3. ( A ∨ ¬ A )
4. A ∧ ( ¬ A ∨ B ) ∧ ( ¬ B ∨ ¬ C ∨ D ) ∧ ( ¬ E ) ∧ ( ¬ A ∨ ¬ C ) ∧ D