Date: Dec 3, 2012 4:44 PM Author: Graham Cooper Subject: Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>> 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)))