Date: Dec 6, 2012 3:37 AM
Author: Graham Cooper
Subject: And Now For my next PROGRAM. . . . . . (~P->F & ~P->~F) -> P
And Now For my next PROGRAM...

.. I will attempt to PROVE ... BY CONTRADICTION..

....

?- t( not(and( add(M,N,SUM) , add(SUM,M,N) )) ).

..that you can't add 2 terms together,

get the SUM, and add it back to the 1st term

to get the 2nd term...

using only these facts printed here for your amusement...

if( bigger(N,M) , not(bigger(M,N)) ).

if( not(bigger(N,M)) , bigger(M,N) ).

if( add(M,N,SUM) , bigger(SUM,M) ).

if( add(M,N,SUM) , bigger(SUM,N) ).

and depth limited MODUS PONENS..

t(NEW,l(L)) :- if(OLD,NEW) , t(OLD,L).

and introducing my new Deduction formula...

t(PC,l(L)) :- if(not(PC),t(F,L)) , if(not(PC),not(F)).

(~P->F & ~P->~F) -> P

I will get PROLOG to LOOK AHEAD...

BY ASSUMING NOT(PC)

... FIND a formula F and also a formula NOT(F)

.... implied by PC

something like

SUM>N & N>SUM ...

THUS PROVING BY CONTRADICTION...

what it was I was about to Prove!.....

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

STAY TUNED.... this is not easy folks!

Do not attempt this at Home...

This could take a week or 3...

COMING

S

O

O

N

on your friendly neighbourhood www.microPROLOG.com

interpreter on the Web!

AUTOMATED PROOF BY CONTRADICTION!

Herc

--

www.microPROLOG.com Beta