
And Now For my next PROGRAM. . . . . . (~P>F & ~P>~F) > P
Posted:
Dec 6, 2012 3:37 AM


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

