Page 111 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS

Unit 6: Formalized Symbolic Logics

Resolution in First-order Logic Notes

In first-order logic, resolution condenses the traditional syllogisms of logical inference down to
a single rule. To understand how resolution works, consider the following example syllogism
of term logic:
All Greeks are Europeans.
Homer is a Greek.
Therefore, Homer is a European.

Or, more generally:
∀x.P(x) ⇒ Q(x)
P(a)
Therefore, Q(a)
To recast the reasoning using the resolution technique, first the clauses must be converted to
conjunctive normal form. In this form, all quantification becomes implicit: universal quantifiers
on variables (X, Y, …) are simply omitted as understood, while existentially-quantified variables
are replaced by Skolem functions.
¬P(x) ∨ Q(x)
P(a)
Therefore, Q(a)
So the question is, how does the resolution technique derive the last clause from the first two?
The rule is simple:
Find two clauses containing the same predicate, where it is negated in one clause but not
in the other.
Perform a unification on the two predicates. (If the unification fails, you made a bad choice
of predicates. Go back to the previous step and try again.)

If any unbound variables which were bound in the unified predicates also occur in other
predicates in the two clauses, replace them with their bound values (terms) there as well.

Discard the unified predicates, and combine the remaining ones from the two clauses into
a new clause, also joined by the “∨” operator.
To apply this rule to the above example, we find the predicate P occurs in negated form
¬P(X)
in the first clause, and in non-negated form
P(a)
in the second clause. X is an unbound variable, while a is a bound value (term). Unifying the two
produces the substitution
X a a
Discarding the unified predicates, and applying this substitution to the remaining predicates
(just Q(X), in this case), produces the conclusion:
Q(a)

LOVELY PROFESSIONAL UNIVERSITY 105