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
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..)
if(..l... , ...r..)
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):
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) )
e(X,rs) :- not(e(X,X)).
thm(e(A,B)) :- 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
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
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
or(X,Y) :- or(X,C) , or(Y,not(C).
Is there are rule like the above format that does cut-elimination?