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 print

the proof as you solve it.

By putting the if( _ , _ ) first

thm(R) :- if(L,R), thm(L)

PROLOG will search for IMPLIES if(_,_) rules

where theorem R is pattern matched to the R in any

if(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 rules

match the HEAD, then the TAIL - L

thm(..r..) :- thm(..l..)

same as

if(..l... , ...r..)

AND MP

thm(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 CONTRADICTION

not(thm(X)) :- thm(X), thm(not(Y)) , thm(Y).

**********************************************

and INTERPRET THE MEANING of

not(thm(X)) as NOT(EXIST(X) X=...)

------

to prove that

not(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 Y

Y should be able to match:

rs e rs

and 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 predicate

notexist( thm(.....

or

not(exist(thm(....

and keep not(thm(X)) == thm(not(X))

but it has to work with

not(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 utilised

or not!!

------------------------------

MP just takes *any* inference rule and applies it with some fact to

match the LHS

or RHS when backward chaining.

I worked out an inference rule (that can work with UNIFY or MP) that

performs 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