Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University 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 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)))
|
|
|
|
