```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.>> ByeRight, but this is just eliminating the global variable to make 'purefunctions'.We did a lot of PROLOG optimisation 20 years ago - Magic SetsAlgorithm!Back then MYACIN was making medical diagnosis in 9ms on parallelcomputers..But UNIFY using binary search on predicate names, optimisation isn't aconcern and accessing the global database will eventually be thememory of the Logic Unit, that is why I returned to the homogeneousformat for portability and possible utility by a planning/nat langsystem.  i.e. convert Winograd's blocks world sentences into thisformat - integrated with subgoal tracing in it's planner moduleSINGLE FORMAL RULE FORMATthm(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 solvingnot( thm( iff( e(X,r) , not(e(X,X) ) ) ).then I can finish Provable Set Theory before I attack Nat Language.Herc--LOGICE(Y) Y={x|P(x)}  <->  DERIVE( E(Y) Y={x|P(x)} )DERIVE(T) <-> DERIVE(a) ^ DERIVE(b) ^ (a^b)->TMATHEMATICSE(Y) Y={x|P(x)}  <->  PRVBLE( E(Y) Y={x|P(x)} )PRVBLE(T) <-> NOT(DERIVE(NOT(T)))
```