PROOF BY RESOLUTION BY MODUS PONENS!

[Graham Cooper]

PROOF BY RESOLUTION is extremely complex!

Logic formulas must go through a series of transformations to all be
in Clause Normal Form.

(p1 v p2 v ~p3 v p4 v ~p5) ..... A NORMAL CLAUSE!

Only OR (v) and NOT (~)
are allowed as the Boolean Parameter Predicates!

Now the THEOREMS are a CONJUNCTION (^) of CLAUSES!

(p1 v p2 v ~p3 v p4 v ~p5) ^ (p2 v p4 v p5) ^ ....

RESOLUTION ==> (p1 v p2 v ~p3 v p4)

p5 is eliminated and the 2 clauses are joined together.

-----------------------------------------

MODUS PONENS is a type of RESOLUTION where one of the clauses is a
single predicate.

(!p1 v p2) ^ (p1)

RESOLUTION/MP ==> (p2)

SINCE (!p1 v p2) is an INFERENCE RULE (p1 -> p2)

p1 is eliminated by EITHER RULE!

-----------------------------------------

This suggests a variation of MODUS PONENS that works like RESOLUTION.

2 EXAMPLE THEOREMS

or( l(z) , q(b) ).
if( l(z) , r(c) ). ...... THIS IS (~l(z) v r(c))

.
.
.

THE LOGIC PROGRAM SO FAR!



f(0).
t(1).
t(X) <- f(f(X)).


wff(X) <- t(X).
wff(X) <- f(X).
what(X,true) <- t(X).
what(X,false) <- f(X).


t(if(X,Y)) <- t(X), t(Y).
t(if(X,Y)) <- f(X), f(Y).
t(if(X,Y)) <- f(X), t(Y).
t(or(X,Y)) <- t(X).
t(or(X,Y)) <- t(Y).
t(and(X,Y)) <- t(X),t(Y).
t(iff(X,Y)) <- t(X),t(Y).
t(iff(X,Y)) <- f(X),f(Y).
t(xor(X,Y)) <- t(X),f(Y).
t(xor(X,Y)) <- f(X),t(Y).

f(if(X,Y)) <- t(X),f(Y).
f(or(X,Y)) <- f(X),f(Y).
f(and(X,Y)) <- f(X).
f(and(X,Y)) <- f(Y).
f(iff(X,Y)) <- t(X),f(Y).
f(iff(X,Y)) <- f(X),t(Y).
f(xor(X,Y)) <- t(X),t(Y).
f(xor(X,Y)) <- f(X),f(Y).


or(R,Q) <- if(L,R), or(L,Q).
or(R,Q) <- if(L,R), or(Q,L).
or(Q,R) <- if(L,R), or(L,Q).
or(Q,R) <- if(L,R), or(Q,L).


t(R) <- if(L,R), t(L).
t(R) <- or(f(L),R), t(L).
t(R) <- or(R,f(L)), t(L).


-------------------------------

The 3rd last line is MODUS PONENS in standard form.
t(R) <- if(L,R) ^ t(L).

The RESOLUTION RULE used here is
or(Q,R) <- if(L,R) ^ or(L,Q).

Now we can ask the Query

GIVEN:
or( l(z) , q(b) ).
if( l(z) , r(c) ).


?- or( q(b) , r(c) ).
YES .......................PROLOG ANSWERS YES!


------------------------

Resolution is the defacto automatic theorem proving method because it
is proven to find the contradiction when a negative theorem is
assumed!

Instead of MODUS PONENS deriving new THEOREMS!

RESOLUTION merely derives DISJUNCTIONS OF THEOREMS! (a type of
theorem)

So here, the theorem prover is working out that:

*EITHER* Q or R is true ... one or the other (or both)

or(Q,R) <- if(L,R), or(L,Q).

So it's an easier inference to make than standard MODUS PONENS.

and complements the "MEANING" of logical OR from it's definition.

t(or(X,Y)) <- t(X).
t(or(X,Y)) <- t(Y).


Herc