Transcript A B - School of Informatics

Prolog and Classical Theorem Proving
Resolution theorem proving viewpoint.
 Natural deduction theorem proving viewpoint.

Logic Programming
School of Informatics, University of Edinburgh
1
Conversion to Clausal Form
Step 1: Eliminate  and  operators.
AB
translates to
(A  B)  (B  A)
AB
translates to
not(A)  B
Logic Programming
School of Informatics, University of Edinburgh
2
Conversion to Clausal Form
Step 2: Move all quantifiers to the left.
not(X.A)
translates to
X.not(A)
not(X.A)
translates to
X.not(A)
(X.A)  B
translates to
X.(A  B)
(X.A)  B
translates to
X.(A  B)
A  (X.B)
translates to
X.(A  B)
A  (X.B)
translates to
X.(A  B)
(X.A)  B
translates to
X.(A  B)
(X.A)  B
translates to
X.(A  B)
A  (X.B)
translates to
X.(A  B)
A  (X.B)
translates to
X.(A  B)
Logic Programming
School of Informatics, University of Edinburgh
3
Conversion to Clausal Form
Step 3: Eliminate all existential quantifiers

Those outside the scope of a universal quantifier
are replaced with Skolem constants.
e.g. X.happy(X) translates to happy(someone)

Those inside the scope of universal quantifiers are
replaced with Skolem functions for which the
arguments are the universally quantified variables.
e.g. X.Y.hates(X,Y) translates to hates(X,enemy(X))
Step 4: Remove universal quantifiers as well
since we can now assume all variables are
universally quantified.
Logic Programming
School of Informatics, University of Edinburgh
4
Conversion to Clausal Form
Step 5: Drive negation inwards to predicates.
not(A  B)
translates to
not(A)  not(B)
not(A  B)
translates to
not(A)  not(B)
not(not(A))
translates to
A
Logic Programming
School of Informatics, University of Edinburgh
5
Conversion to Clausal Form
Step 6: Bundle disjunctions together.
A  (B  C)
translates to
(A  B)  (A  C)
Step 7: Convert each disjunction bundle to a set.
AB
translates to
{A,B}
Step 8: Convert top-level conjunction to a set.
{A,…}  {B,…}
translates to
{ {A,…}, {B,…} }
Logic Programming
School of Informatics, University of Edinburgh
6
Example of Clausal Form Translation
X.((lecturer(X)  not(logic_programmer(X))  kindly(X)) 
lecturer(dave)  not(kindly(dave))
X.(not(lecturer(X)  not(logic_programmer(X))  kindly(X)) 
lecturer(dave)  not(kindly(dave))
X.(not(lecturer(X))  not(not(logic_programmer(X)))  kindly(X)) 
lecturer(dave)  not(kindly(dave))
X.(not(lecturer(X))  logic_programmer(X)  kindly(X)) 
lecturer(dave)  not(kindly(dave))
(not(lecturer(X))  logic_programmer(X)  kindly(X)) 
lecturer(dave)  not(kindly(dave))
{ {not(lecturer(X)), logic_programmer(X), kindly(X)},
{lecturer(dave)}, {not(kindly(dave))} }
Logic Programming
School of Informatics, University of Edinburgh
7
A Resolution Proof
To prove logic_programmer(dave) from :
{ {not(lecturer(X)),logic_programmer(X),kindly(X)},
{lecturer(dave)},
{not(kindly(dave))} }
{not(logic_programmer(dave))}
{not(lecturer(X)),
logic_programmer(X),
kindly(X)}
{not(lecturer(dave)),
kindly(dave)}
{kindly(dave)}
{lecturer(dave)}
{not(kindly(dave))}
{}
Contradiction
Logic Programming
School of Informatics, University of Edinburgh
8
Prolog Viewed as Resolution Proof
p(X) :- q(X), r(X).
q(a).
r(a).
| ?- p(a).
p(X)  q(X)  r(X).
q(a).
r(a).
{not(p(a))}
{ {p(X), not(q(X)), not(r(X))}
{q(a)},
{r(a)} }
{p(X), not(q(X)), not(r(X))}
{not(q(a)), not(r(a))}
{q(a)}
{not(r(a))}
yes
{}
{r(a)}
Contradiction
Logic Programming
School of Informatics, University of Edinburgh
9
Prolog as a Form of Natural Deduction
Sub-proofs
Proof
F true
AF
F AB
F A F B
F A
F AB
F AB
F B
ABF F
F A
plus negation as failure:
F A
F not(A)
1
2
3
4
B
5
Logic Programming
School of Informatics, University of Edinburgh
10
A Prolog Natural Deduction Proof
F
F = { p(a)  true,
p(f(X))  p(X) }
p(f(f(a)))
5
p(f(f(a)))  p(f(a))  F
F
p(f(a))
5
p(f(a))  p(a)  F
F
p(a)
5
p(a)  true  F
F
true
1
Logic Programming
School of Informatics, University of Edinburgh
11
Divergences
Some proof rules in classical natural deduction
aren’t used in Prolog.
F
F
C
AB
A or B  F [ A|F ]
[ A|F ] B
C [ B|F ]
C
but one can get similar effects by different means:
g(X1,…,Xm)  p(X1,…,Xn) or q(Xn+1,…,Xm)  F
then use g(…) instead of (p(…) or q(…))
Use equivalence of A  B to not(A  not(B))
Logic Programming
School of Informatics, University of Edinburgh
12