Page 112 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS

Introduction to Artificial Intelligence & Expert Systems

Notes For another example, consider the syllogistic form:
All Cretans are islanders.
All islanders are liars.
Therefore all Cretans are liars.

Or more generally,
∀X P(X) → Q(X)
∀X Q(X) → R(X)
Therefore, ∀X P(X) → R(X)
In CNF, the antecedents become:
¬P(X) ∨ Q(X)

¬Q(Y) ∨ R(Y)
Note that the variable in the second clause was renamed to make it clear that variables in
different clauses are distinct.
Now, unifying Q(X) in the first clause with ¬Q(Y) in the second clause means that X and Y
become the same variable anyway. Substituting this into the remaining clauses and combining
them gives the conclusion:
¬P(X) ∨ R(X)

The resolution rule, as defined by Robinson, also incorporated factoring, which unifies two
literals in the same clause, before or during the application of resolution as defined above. The
resulting inference rule is refutation complete, in that a set of clauses is unsatisfiable if and only
if there exists a derivation of the empty clause using resolution alone.

6.6.2 The Resolution Principle

The resolution principle, due to Robinson (1965), is a method of theorem proving that proceeds
by constructing refutation proofs, i.e., proofs by contradiction. This method has been exploited
in many automatic theorem provers. The resolution principle applies to first-order logic formulas
in Solemnized form. These formulas are basically sets of clauses each of which is a disjunction of
literals. Unification is a key technique in proofs by resolution.

If two or more positive literals (or two or more negative literals) in clause are unifiable and η is
their most general unifier, then S is called a factor of s. For example, P(x) ∨ ¬ Q(f(x), b) ∨ P(g(y))
η
is factored to P(g(y)) ∨ ¬ Q(f(g(y)), b). In such a factorization, duplicates are removed. Let S and
1
S be two clauses with no variables in common, let S contain a positive literal L , S contain a
2 1 1 2
negative literal L , and let η be the most general unifier of L and L . Then
2 1 2
(S η – L η) U (S η – L η)
1 1 2 2
is called a binary resolvent of S and S . For example, if S = P(x) ∨ Q(x) and S = ¬P(a) ∨ R(y), then
1 2 1 2
Q(a) ∨ R(y) is their binary resolvent.
A resolvent of two clauses S and S is one of the four following binary resolvents.
1 2
1. A binary resolvent of S and S .
1 2
2. A binary resolvent of S and a factor of S .
1 2
3. A binary resolvent of a factor of S and S .
1 2
4. A binary resolvent of a factor of S and a factor of S .
1 2

106 LOVELY PROFESSIONAL UNIVERSITY