Transcript Lecture Notes

Formal Aspects of
Computer Science - Week 8
The Law of Resolution and
the Resolution Procedure
Lee McCluskey, room 2/07
Email [email protected]
http://scom.hud.ac.uk/scomtlm/cia2326/
Resolution Refutation
Recap
Last Week we covered:
-Conversion to Clausal Form
-Unification
..as both these are needed in the law of inference
called Resolution.
Resolution Refutation
The Law of (Binary) Resolution
Two PARENT clauses w1 and w2 infer a CHILD clause wr if
there are two (*) positive literals L and M such that
• L is a member of w1
• ~ M is a member of w2
• {L,M} unify under some substitution sequence S.
Remembering that clauses are sets of literals, we can deduce
wr = [ (w1 union w2) minus { L, ~ M } ]/S.
The law also assumes that each clause has unique variable
letters. This does not restrict its generality because variables
in separate clauses are independent.
* The general law of resolution allows more that 1 literal to be
unified in each clause
Resolution Refutation
Motivation
This law is often embodied is a “proof procedure”
called Resolution Refutation which is SOUND and
COMPLETE.
Resolution Refutation
Proof by Refutation
(Sometimes called Proof by Contradiction or
Reductio ad Absurdum)
This is an efficient way of reasoning:
assume what we are trying to prove is FALSE, then get a
CONTRADICTION
=> what we were trying to prove is TRUE.
Imagine we know Wff1 to be TRUE and we want to prove
Wff2 logically follows from Wff1. If we can derive a
contradiction from
(Wff1 & ~Wff2)
then assuming Wff1 is TRUE we know that Wff2 logically
follows from Wff1, or written in logic:
Wff1 |- Wff2
Resolution Refutation
Resolution Refutation
Resolution is a super law of inference which
- can easily be automated
- when used in refutation mode it is COMPLETE - it can deduce
any Wff that logically follows.
- is the basis for Prolog’s computation
Resolution Refutation: To PROVE Wff2 FROM Wff1
1. Translate Wff1 to CLAUSAL FORM
2. Translate ~ Wff2 to CLAUSAL FORM
3. Get contradiction from 1 + 2 using Resolution
…. It follows that Wff1 |- Wff2
Resolution Refutation
Back to Student Example …
S = student, D = academic, T = teaches
Ax ( S(x)=>D(x) ) ;
Ax ( (Ey (T(x,y) & D(y) ) => D(x) )
S(Fred) ; T(Jeff,Fred)
CLAUSAL FORM:
1. ~S(z) V D(z)
2. ~T(x,y) V ~D(y) V D(x)
3. S(Fred)
4. T(Jeff,Fred)
Resolution Refutation
Example
1. ~S(x) V D(x)
3. S(Fred)
Subs = Fred / x
D(Fred)
2. ~T(x,y) V ~D(y) V D(x)
Subs = Fred / y
5. ~D(Jeff)
~T(x,Fred) V D(x)
Subs = Jeff / x
~T(Jeff,Fred)
4. T(Jeff,Fred)
..So D(Jeff) follows from our premises
Resolution Refutation
Summary
Resolution is a law of inference that is based on:
- Wffs in CLAUSAL FORM
- The method of UNIFICATION of literals
Resolution Refutation is a deduction procedure that is
 COMPLETE
 amenable to AUTOMATION
 PROLOG works using a “single literal depth-first” (SLD)
resolution refutation procedure
Resolution Refutation