Page 110 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS

Introduction to Artificial Intelligence & Expert Systems

Notes A Resolution Technique

When coupled with a complete search algorithm, the resolution rule yields a sound and complete
algorithm for deciding the satisfiability of a propositional formula, and, by extension, the
validity of a sentence under a set of axioms.
This resolution technique uses proof by contradiction and is based on the fact that any sentence
in propositional logic can be transformed into an equivalent sentence in conjunctive normal
form. The steps are as follows:
All sentences in the knowledge base and the negation of the sentence to be proved (the
conjecture) are conjunctively connected.
The resulting sentence is transformed into a conjunctive normal form with the conjuncts
viewed as elements in a set, S, of clauses.

For example (A ∨ A ) ∧ (B ∨ B ∨ B ) ∧ (C ) gives rise to the set S = {A ∨ A , B ∨ B ∨ B , C }.
1 2 1 2 3 1 1 2 1 2 3 1
The resolution rule is applied to all possible pairs of clauses that contain complementary
literals. After each application of the resolution rule, the resulting sentence is simplified
by removing repeated literals. If the sentence contains complementary literals, it is
discarded (as a tautology). If not, and if it is not yet present in the clause set S, it is added
to S, and is considered for further resolution inferences.
If after applying a resolution rule the empty clause is derived, the original formula is
unsatisfiable (or contradictory), and hence it can be concluded that the initial conjecture
follows from the axioms.

If, on the other hand, the empty clause cannot be derived, and the resolution rule cannot be
applied to derive any more new clauses, the conjecture is not a theorem of the original
knowledge base.

One instance of this algorithm is the original Davis – Putnam algorithm that was later refined
into the DPLL algorithm that removed the need for explicit representation of the resolvents.
This description of the resolution technique uses a set S as the underlying data-structure to
represent resolution derivations. Lists, Trees and Directed Acyclic Graphs are other possible and
common alternatives. Tree representations are more faithful to the fact that the resolution rule
is binary. Together with a sequent notation for clauses, a tree representation also makes it clear
to see how the resolution rule is related to a special case of the cut-rule, restricted to atomic
cut-formulas. However, tree representations are not as compact as set or list representations,
because they explicitly show redundant subderivations of clauses that are used more than once
in the derivation of the empty clause. Graph representations can be as compact in the number of
clauses as list representations and they also store structural information regarding which clauses
were resolved to derive each resolvent.

a ∨ , b ¬ a ∨ c
Example:
b ∨ c
In plain language: Suppose a is false. In order for the premise a ∨ b to be true, b must be true.
Alternatively, suppose a is true. In order for the premise ¬a ∨ c to be true, c must be true.
Therefore regardless of falsehood or veracity of a, if both premises hold, then the conclusion
b ∨ c is true.

104 LOVELY PROFESSIONAL UNIVERSITY