Page 109 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS
P. 109
Unit 6: Formalized Symbolic Logics
4. ¬r Modus tollens using Step 2 and 3 Notes
5. ¬r → s Hypothesis
6. s Modus ponens using Step 4 and 5
7. s → t Hypothesis
8. s Modus ponens using Step 6 and 7
Self Assessment
State whether the following statements are true or false:
9. Horn problems are difficult than non-Horn problems.
10. Transformation rule is the act of drawing a conclusion based on the form of premises
interpreted as a function.
6.6 Resolution Logic
In mathematical logic and automated theorem proving, resolution is a rule of inference leading
to a refutation theorem-proving technique for sentences in propositional logic and first-order
logic. In other words, iteratively applying the resolution rule in a suitable way allows for
telling whether a propositional formula is satisfiable and for proving that a first-order formula
is unsatisfiable; this method may prove the satisfiability of a first-order satisfiable formula, but
not always, as it is the case for all methods for first-order logic. Resolution was introduced by
John Alan Robinson in 1965.
The clause produced by a resolution rule is sometimes called a resolvent.
6.6.1 Resolution Rule
The resolution rule in propositional logic is a single valid inference rule that produces a new
clause implied by two clauses containing complementary literals. A literal is a propositional
variable or the negation of a propositional variable. Two literals are said to be complements if
one is the negation of the other (in the following, is taken to be the complement to b ). The
j
resulting clause contains all the literals that do not have complements. Formally:
∨ ∨ a ∨ ∨ b
1 i n 1 j m
a ∨K a ∨K , b ∨K b ∨K
1 i− 1 i+ 1 n 1 j− 1 j+ 1 m
a ∨K ∨ a ∨ a ∨K ∨ a ∨ b ∨K ∨ b ∨ b ∨K ∨ b
where
all as and bs are literals,
a is the complement to b , and
i j
the dividing line stands for entails
The clause produced by the resolution rule is called the resolvent of the two input clauses.
When the two clauses contain more than one pair of complementary literals, the resolution rule
can be applied (independently) for each such pair; however, the result is always a tautology.
Modus ponens can be seen as a special case of resolution of a one-literal clause and a two-literal
clause.
LOVELY PROFESSIONAL UNIVERSITY 103
