Date: Dec 4, 2012 7:44 PM
Author: Graham Cooper
Subject: Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>

[JAN]

> >      thm(C) :- if((A,B),C), thm(A), thm(B).
>
> This is my whole proof ideology!
>
> To construct a Directed Acyclic Graph from the Theorem back to axioms,
> I call it binary modus ponens.


or Dual Tail End Recursion!


[JAN]

> > Then you should be able to prove:
>
> >        p, p -> q, p -> r, q&r -> s |- s
>



p->q
/ \
p s
\ /
p->r

Hence the D.A.G. instead of the traditional linear proof meta-
predicate introduced by Godel.

Herc
--
E(Y) Y={x|P(x)} <-> DERIVE( E(Y) Y={x|P(x)} )
DERIVE(T) <-> DERIVE(a) ^ DERIVE(b) ^ (a^b)->T