Transcript Lecture Notes

Formal Aspects of Computer
Science - Week 10
An Automated Theorem Prover
Lee McCluskey, room 2/07
Email [email protected]
http://scom.hud.ac.uk/scomtlm/cia2326/
Resolution Refutation
Recap
Last Week
- First Order Logic - Relationship with Prolog
- How to get answers from Resolution Refutation
(and Prolog)
- The Martians Example
This week – An Automated Theorem Prover (ATP)
Resolution Refutation
Automated Theorem Proving
-
Using a tool to show that a wff1 logically follows
from a wff2
- Of great interest in problem solving, proving
theorems, proving software etc
- NOTE proof and correctness is always RELATIVE.
You can prove w1 follows from w2 is correct, but
you can’t prove simply “w1 is correct”.
So – you could prove a program is correct with respect
to a specification, but never “a program is correct”.
Resolution Refutation
Automated Theorem Proving Strategies
A membership procedure is DECIDABLE if there is an
algorithm which can deliver a solution (yes or no)
in a finite no. of steps
Theoretically, proof that w1 follows from w2 is “SEMIDECIDABLE” in the sense that
- if you know w1 follows from w2 then we can use
resolution to deduce wffs from w2 and know that
eventually w1 will be produced
- If you DON’T KNOW that w1 follows from w2,
then there is no effective procedure that can let us
know the answer for all possible inputs 
Resolution Refutation
Automated Theorem Proving Strategy
We try to embed strategies into help with the problem
of deciding which of possibly many clause
pairs (parents) should be resolved next. Some
common ones:
"Set of Support" Strategy:
use a parent which is either an element of the negated
query clause or an ancestor of one.
“Unit Preference” Strategy
use clauses which contain 1 literal if possible
Resolution Refutation
Automated Theorem Prover
:- [cf,ur,testmartians].
predicate prove(depth,query,wff).
cf is the code to change to clausal form
ur is the code that does resolution
testmartians contains a particular problem
“depth” is the search limit of the ATP
Resolution Refutation
Automated Theorem Prover
To use you must learn the syntax for writing the Wffs in- to
do this look at examples..
p53:-prove(9,
all(x1,green(x1)->friendly(x1) ),
( all(x2, green(x2)->antennae(x2)) &
all(x3, all(x4, child(x4,x3)->antennae(x4))
-> friendly(x3)) &
all(x5, exists(x6, child(x5,x6)&green(x6))
->green(x5) )
)
).
Resolution Refutation
Automated Theorem Prover
DEMO …………
Resolution Refutation
Summary
Proof is semi decidable
Proof tools use heuristics and strategies such as set-of-support
You have been emailed an ATP written in Prolog
Resolution Refutation