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