Slide 14.7: Examples of Horn clauses (cont.)
Slide 14.9: Resolution (cont.)
Home

Resolution

A procedural interpretation can be applied to Horn clauses if they are presented in reverse order: 
     b ← a1 ∧ a2 ∧ a3 ∧ … ∧ an.
which can be viewed as a definition of procedure b: the body of b is given by the body of the clause. b is called the head of the clause, and the a1 … an is the body of the clause. Also, the “and” connectives between the ai are usually dropped and just separate them with commas: 
     b ← a1, a2, a3, …, an.
Resolution is an inference rule for Horn clauses:
The resolution principle is a method of theorem proving that proceeds by constructing refutation proofs, i.e., proofs by contradiction.
That is if we have two Horn clauses, and the head of the first clause is matched with one of the statements in the body of the second clause, then the first clause can be used to replace its head in the second clause by its body: 
     a ← a1, a2, a3, …, an.
     b ← b1, b2, b3, …, bm.
and bi matches a, then we can infer the clause 
     b ← b1, …, bi-1, a1, …, an, …, bi+1, …, bm.
For example, the final clause is inferred from the first two clauses: This is precisely the inference rule given previously.