The Math Forum

Search All of the Math Forum:

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

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Replies: 2   Last Post: Dec 3, 2012 4:44 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View  
Graham Cooper

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

On Dec 3, 8:29 pm, Jan Burse <> wrote:
> The formal system G3 from Kleene is based on cut-elimination.
> Means it does not make use of modus ponens. Modus ponens make
> backward chaining a little harder since it introduces an
> unknown formula. The inference rule for modus ponens
> would be (in the spirit of G3):
>       G |- A      G |- A -> B
>       ----------------------- (MP)
>              G |- B
> If you write this as a thm/1 Prolog clause, you get:
>      thm(S,B) :- thm(S,A), thm(S,(A->B)).
> And you see that the variable A is fresh, i.e. only occurs
> in the body of the Prolog clause but not in the head. On the
> other hand in the cut eliminate system, you find not a single
> Prolog clause where a variable representing a formula is fresh:
>     thm(S, A) :- member(A, S).
>     thm(S, (A->B)) :- thm([A|S], B).
>     thm(S, C) :- select((A->B), S, T), thm(S, A), thm([B|T], C).
> Some call such a formal system analytic, since it is only
> based on the sub formulas of the given problem, and does not
> invent new formulas. Cut elimination shows that the analytic
> sequent system is as powerful as the corresponding Hilbert
> style system with modus ponens.
> But what logic is the propositional implicational fragment of
> G3. Well it is minimal logic. In the higher order case you
> can keep it like that and add typed principles like
> comprehension or choice, and get some powerful systems on
> equal foot with FOL and more.
> Or you can try to add new logical principles, to get for
> example classical logic. The difficulty here is also to
> keep the system analytic. For example the following inference
> rule is not analytic, since introduce a new formula L:
>         G, ~R |-  L      G, ~R |- ~L
>         ----------------------------
>                  G |- R
> But adding the following analytical principle is much easier
> and turns the minimal logic into intuitionist logic:
>         G |- f
>         ------
>         G |- A
> Or as Prolog clause:
>        thm(S, A) :- thm(S, f).
> You can also add the following analytical principle, to
> arrive at a paraconsistent logic from the minimal logic:
>         G, (A->f) |- A
>         --------------
>         G |- A
> Or as Prolog clause:
>        thm(S, A) :- thm([(A->f)|S], A).
> If you add both you get classical logic.
> Bye

Right, but this is just eliminating the global variable to make 'pure

We did a lot of PROLOG optimisation 20 years ago - Magic Sets

Back then MYACIN was making medical diagnosis in 9ms on parallel

But UNIFY using binary search on predicate names, optimisation isn't a
concern and accessing the global database will eventually be the
memory of the Logic Unit, that is why I returned to the homogeneous
format for portability and possible utility by a planning/nat lang
system. i.e. convert Winograd's blocks world sentences into this
format - integrated with subgoal tracing in it's planner module


thm(greater(X,Y), 1) <- greater(X,Y).


thm(if(X,Y), step(S)) <- not(thm(X,S)).
thm(if(X,Y), step(S)) <- thm(Y,S).
thm(and(X,Y), step(S)) <- thm(X,S) , thm(Y,S).
thm(or(X,Y), step(S)) <- thm(X,S).
thm(or(X,Y), step(S)) <- thm(Y,S).


thm(not(X), step(S)) <- not(thm(X,S)).

I'll have another go at solving

not( thm( iff( e(X,r) , not(e(X,X) ) ) ).

then I can finish Provable Set Theory before I attack Nat Language.

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

E(Y) Y={x|P(x)} <-> PRVBLE( E(Y) Y={x|P(x)} )

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

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2018. All Rights Reserved.