
Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Posted:
Dec 4, 2012 6:16 PM


On Dec 5, 8:05 am, Jan Burse <janbu...@fastmail.fm> wrote: > Graham Cooper schrieb: > > > By putting the if( _ , _ ) first > > > thm(R) : if(L,R), thm(L) > > I guess you mean: > > thm(B) : thm(if(A,B)), thm(A)
I can add
thm( if(X,Y) ) : if(X,Y)
to bring if statements into the theory, but you can also have inference rules at a different level to theorems (a popular point from GG)
> > Only them it is modus ponens. Namely then you > have the Hilbert style inference rule: > >  A>B  A >  >  B > > But if you have: > > thm(B) : if(A,B), thm(A). > > Then this is something else. I am not sure what it > should be. You have to explain. It resembles > the Prolog forward chaining vanilla interpreter > which has (simplified version without oneormore > and already): > > solved(B) : clause(B,A), solved(A). > > Note clause/2 is the mirror of if/2. That is > why the arguments are reversed. > > But the inference rule, which the forward chaining > vanilla interpreter is based on, is not modus ponens. > It is the (>L) rule of the cuteliminated sequent > calculus. Namely this rule reads, without Dragalins > optimization, i.e. the original Kleene G3: > > G, A > B  A G, A > B, B  C >  (>L) > G, A > B  C > > Forward chaining is now a special case of the above rule, > when you have in G already the solved unit clause A. We > then have: > > G', A, A > B  A G', A, A > B, B  C >  (>L) > G', A, A > B  C > > We can close the left branch via the (id) rule, since A > is already part of G. > >  (id) > G', A, A > B  A G', A, A > B, B  C >  (>L) > G', A, A > B  C > > So basically we go from: > > G', A, A > B  C > > To the following via backward chaining: > > G', A, A > B, B  C > > So we started with A, and we added B, because there was > a rule A > B. This is the backward chaining explanation > of forward chaining. Of course A has been a theorem already, > and B is a theorem now, by means of the (id) rule again: > >  (id) > G', A, A > B  A > >  (id) > G', A, A > B, B  B > > But there is one drawback of this approach, during back > tracking you loose B again. So that the method is a little > forgetful, and recomputes a lot of things again an > again. But if you add: > > 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.
(It ends up one of A or B is usually an inference rule and it just applies standard MP  going round is circles!)
I should be able to construct sets without contradictions this way.
LOGIC E(Y) Y={xP(x)} <> DERIVE( E(Y) Y={xP(x)} ) DERIVE(T) <> DERIVE(a) ^ DERIVE(b) ^ (a^b)>T
MATHEMATICS E(Y) Y={xP(x)} <> PRVBLE( E(Y) Y={xP(x)} ) NOT(PRVBLE(T)) <> DERIVE(NOT(T))
since DERIVE(NOT( EXIST(russellset) ))
Going back to my previous MODUS PONENS system.
 if( and(X , Y ), or(X,Y) ). if( and(not(X) , not(Y) ), not(or(X,Y)) ). if( and(not(X) , Y ), or(X,Y) ). if( and(X , not(Y) ), or(X,Y) ).
if( and(not(X) , not(Y) ), not(and(X,Y)) ). if( and(not(X) , Y ), not(and(X,Y)) ). if( and(X , not(Y) ), not(and(X,Y)) ).
if( and(X , Y ), if(X,Y) ). if( and(not(X) , not(Y) ), if(X,Y) ). if( and(not(X) , Y ), if(X,Y) ). if( and(X , not(Y) ), not(if(X,Y)) ).
if( and(X , Y ), iff(X,Y) ). if( and(not(X) , not(Y) ), iff(X,Y) ). if( and(not(X) , Y ), not(iff(X,Y)) ). if( and(X , not(Y) ), not(iff(X,Y)) ).
if( and(if(A,B) , if(B,C)), if(A,C) ).
if( not(not(X)) , X ). if( not(and(X,Y)) , or(not(X),not(Y)) ). if( not(or(X,Y)) , and(not(X),not(Y)) ).
and(X,Y) : t(X), t(Y). and(X,not(Y)) : t(X), not(Y). and(not(X),not(Y)) : not(X), not(Y). and(not(X),Y) : not(X), t(Y).
t(and(X,Y)) : and(X,Y).
t(R) : t(L), if(L,R).
t(less(X,Y)) : less(X,Y). less(0,X). if( and(less(X,Y) , less(Y,Z)) , less(X,Z) ).
Predicates are themselves constructed using
if( and( _,_ ) , _ )
and so are the arithmetic inferences etc..
and(X,Y) : thm(X) , thm(Y)
does the cartesian calculation depth first in Unify.
> > Then you should be able to prove: > > p, p > q, p > r, q&r > s  s > > But for ternary conjunction you would need to add: > > thm(D) : if((A,B,C),D), thm(A), thm(B), thm(C). > > And for quaternary conjunction you would need to add: > > thm(E) : if((A,B,C,D),E), thm(A), thm(B), thm(C), thm(D). > > And so on. One solution to make it not forgetful, is the > forward chaining rule I have given: > > : forward solved/1. > > solved(H) : solved(A), forward(H,B), > oneormany(A,B,C), already(C). > > Important thing is here the forward declaration, so > that solved facts do not become forgetful. If it is not > forgetful, we can get away with checking only one > newly arrived solved/1 fact and check the rest via the > old solved/1 facts. > > Lets introduce: > > thm_arrived: new arrived solved/1 fact. > thm_new: delta of solved/1 facts. > thm_memory: old solved/1 facts. > > The above solved/1 forward chaining rule then does nothing > else than: > > thm_new(B) : if(A,B), thm_arrived(A). > thm_new(C) : if((A,B),C), thm_arrived(A), thm_memory(B). > thm_new(C) : if((A,B),C), thm_memory(A), thm_arrived(B). > thm_new(C) : if((A,B),C), thm_arrived(A), thm_arrived(B). > Etc.. > > And the interpreter does nothing else than: > > 1) Pick the newest thm_new/1, retract it and assert > it as thm_arrived/1. > > 2) Invoke all forward rules, and compute the new thm_new/1 > and assert them. > > 3) Retract the thm_arrived/1 and assert it as thm_memory/1. > > 4) Continue with 1). > > The Craft of Prolog has a section about delta fixpoint calculation. > But I did not yet verify that it really matches the above. There > are also a lot of other papers around about delta calculations. > > Using memory and delta computation is not mandatory. You can > also do it as you do, via the backward chaining interpretation > of forward chaining. But a non forgetful implementation is > especially useful, if the derived thm/1 is used in multiple > places, for example a cell in a chart parser. > >
Right, but with a billion records in MySQL and logarithmic slowing you could just turn off garbage collection after running queries, a crude learning of facts the more queries that you ask it.
Herc

