The algorithm terminates since there every iteration of the while-loop increases the number of marked atoms, and the Horn formula can only refer to a finite number of propositional atoms.
In a Horn clause of the form ( p1 ∧ p2 ∧ ... ∧ pn → q ) we shall find it convenient to refer to p1 ∧ p2 ∧ ... pn as the premise and q as the conclusion.
If T
('top') does not occur as the premise of a clause of the form (T
→ p) in a Horn formula, then setting all the propositional atoms in the formula to false
will satisfy it. (Since it renders the implication in every clause vacuously true, as its premise is false.)
Suppose then that T
does occur as the premise of a clause of the form (T
→ p) in a Horn formula. It then follows by a simple inductive argument that - in any assignment of truth values that could potentially satisfy the formula - all the propositional atoms that are marked by the HORN algorithm must be set to true
.
Suppose then that all the marked atoms have been set to true
, and consider the assignment of truth values that sets the remaining propositional atoms in the formula to false
.
The only circumstances in which a Horn clause within the formula is not satisfied is when we have been obliged to set all the propositional atoms in the premise of the clause to true
, and its conclusion is the unsatisfiable formula 'bottom'. This is the case because if we have been obliged to set all the propositional atoms in the premise of the clause to true
, and its conclusion is a propositional atom, this atom will have been marked in the while-loop and hence will be set to true
.
This justifies the criterion used in the algorithm to determine whether or not the given Horn formula is satisfiable.