|
|
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
|
|
