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..) 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..