Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math

Topic: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Replies: 6   Last Post: Dec 5, 2012 2:39 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,295
Registered: 5/20/10
Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Posted: Dec 4, 2012 6:16 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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 cut-eliminated 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={x|P(x)} <-> DERIVE( E(Y) Y={x|P(x)} )
DERIVE(T) <-> DERIVE(a) ^ DERIVE(b) ^ (a^b)->T

MATHEMATICS
E(Y) Y={x|P(x)} <-> PRVBLE( E(Y) Y={x|P(x)} )
NOT(PRVBLE(T)) <-> DERIVE(NOT(T))

since DERIVE(NOT( EXIST(russell-set) ))


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




Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.