On Dec 13, 1:41 pm, Dan Christensen <Dan_Christen...@sympatico.ca> wrote: > On Dec 12, 6:54 pm, Jan Burse <janbu...@fastmail.fm> wrote: > > Here is an example where the above method gives a false > > positive: > > > Your system should be able to prove: > > > ~p & (~p -> p) -> ~p > > Easy. > > 1 ~P & [~P => P] > Premise > > 2 ~P > Split, 1 > > 3 ~P & [~P => P] => ~P > Conclusion, 1 > > > But we do not have: > > > ~p & (~p -> p) |/- p > > > In fact by modus ponens it is easy to see that p > > derives from ~p & (~p -> p). > > Also easy. > > 1 ~P & [~P => P] > Premise > > 2 ~P > Split, 1 > > 3 ~P => P > Split, 1 > > 4 P > Detach, 3, 2 > > 5 ~P & [~P => P] => P > Conclusion, 1 > > Sorry, I don't see your point, Jan.
3 ~P & [~P => P] => ~P 5 ~P & [~P => P] => P
This would definitely qualify for G.I.G.O. though!
So is a MODEL FINDER required to detect this contradiction?
I would have thought a MP style contradiction rule would work..
~p->f & ~p->~f ---------------- p
I think I can get this running in the same Theorem Prover program using a transitive -> rule.
1st I want to test out AXIOM BASED Modus Ponens with Transitive Implication.
BACKWARD CHAINED - FORWARD BRANCHING MP
t(NEW,l(L)) :- trif(AXIOM,NEW,L), t(AXIOM,1).
TRANSITIVE IF trif( OLD , NEW , l(L) ) :- if( OLD , NEW ). trif( OLD , NEW , l(L) ) :- if( OLD , MID ) , trif( MID, NEW , L ).
STANDARD MP t(NEW,l(L)) :- if(OLD,NEW) , t(OLD,L).
branches lower and lower eventually reaching an axiom.