```Date: Dec 4, 2012 4:22 PM
Author: Graham Cooper
Subject: Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>

On Dec 4, 11:07 pm, Jan Burse <janbu...@fastmail.fm> wrote:> Graham Cooper schrieb:>> > I was referring to having no 'fresh' variables on the RHS.>> > This is just a way of matching any formula in the database as the VARS> > stand for theorems.>> > thm(R) :- thm(L) , if(L,R)>> > But UNIFY will execute MODUS PONENS built in (with a depth limit)> > so I will see if a separate control is needed.>> In the above L will be fresh. So the search of a> proof will not be goal directed anymore. It will look> for any L independent of R.>> On the other hand in g3i.p we have goal directedness:>>         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).>> And also the extension to g3c.p does more or less:>>         thm(S, _) :- thm(S, f).>         thm(S, A) :- thm([(A->f)|S], A).>But how can you avoid searching for theorems,what is the complexity reduction?it looks like you are just constructing a list to printthe proof as you solve it.By putting the if( _ , _ )  firstthm(R) :- if(L,R), thm(L)PROLOG will search for IMPLIES if(_,_) ruleswhere  theorem R is pattern matched to the R in anyif(L,R)then if successful, use_those_bindings to find an L.so neither if(L,R) or thm(L) are completely fresh.that is actually backward chaining MP,the same process used as PROLOG rulesmatch the HEAD, then the TAIL - Lthm(..r..) :- thm(..l..)same asif(..l... , ...r..)AND MPthm(R) :- if(L,R), thm(L)> But I wouldn't recommend using g3c.p, there are better> algorithms to search for classical proofs only. I am> using it to find out if there is a proof that is classical,> intuitionist, paraconsistent or minimal. For example if I> find a proof that doesn't make use of the two extension for> classical, I know it is from minimal logic.>> But if you are fond of modus ponens, you could also follow> the following approach.>>    Step 1) Find a proof in a cut-free sequent calculus>>    Step 2) Convert the cut-free sequent calculus proof>            into a Hilbert style proof with modus ponens.>> A method for step 2) was invented by M.Sch nfinkel in> 1924. It goes nowadays under the name Braket Abstraction.> Here you see the approach for a simple classical example> (and thus introducing new combinators):>> http://stackoverflow.com/questions/1581256/hilbert-system-automate-pr...>> Bye>OK, supercombinators are a bit low level for my work..I might try:**********************************************PROOF BY CONTRADICTIONnot(thm(X))  :-  thm(X),  thm(not(Y)) , thm(Y).**********************************************and INTERPRET THE MEANING ofnot(thm(X))  as NOT(EXIST(X) X=...)------to prove thatnot(EXIST(rs)  Xers <-> not(XeX) )i.e.e(X,rs) :- not(e(X,X)).thm(e(A,B)) :- e(A,B).?- not(thm(e(A,B))--------------so not(Y) and YY should be able to match:rs e rsand it should prove Russells Set doesn't exist.although some forward chaining might be necessary to bind  X=rs-----------I might be better introducing a predicatenotexist( thm(.....ornot(exist(thm(....and keep not(thm(X)) ==  thm(not(X))but it has to work withnot(provable(X)) == thm(not(X))isset( X ) :- provable(X)****I think some Quantifier rules without the QUANTIFIED TERM can do this.A(X) not(f(X))  -->  not( E(X)  f(X) )just use a weak QUANTIFIER that means  (for some term..)all( not( F ))  -->  not( exist( F ) )I'm not sure if the above Claytons quantifier formula can be utilisedor not!!------------------------------MP just takes *any* inference rule and applies it with some fact tomatch the LHSor RHS when backward chaining.I worked out an inference rule (that can work with UNIFY or MP) thatperforms pseudo-resolution.or(X,Y)  :-  or(X,C) , or(Y,not(C).Is there are rule like the above format that does cut-elimination?Herc
```