Drexel dragonThe Math ForumDonate to the Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Topic: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Replies: 6   Last Post: Dec 5, 2012 2:39 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,359
Registered: 5/20/10
Re: LOGICAL NEGATION working in PROLOG! <<Using Peano Arithmetic>>
Posted: Dec 4, 2012 4:22 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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

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


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

?- 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(.....

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?


Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum 1994-2015. All Rights Reserved.