Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.



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 cutelimination. > 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([AS], B). > thm(S, C) : select((A>B), S, T), thm(S, A), thm([BT], 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={xP(x)} <> DERIVE( E(Y) Y={xP(x)} ) DERIVE(T) <> DERIVE(a) ^ DERIVE(b) ^ (a^b)>T
MATHEMATICS E(Y) Y={xP(x)} <> PRVBLE( E(Y) Y={xP(x)} ) PRVBLE(T) <> NOT(DERIVE(NOT(T)))



