Search All of the Math Forum:

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

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

 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

On Dec 3, 8:29 pm, Jan Burse <janbu...@fastmail.fm> 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
functions'.

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

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

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

SINGLE FORMAL RULE FORMAT

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.

Herc
--
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)} )
PRVBLE(T) <-> NOT(DERIVE(NOT(T)))