Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: PREDICATE CALCULUS 2
Replies: 23   Last Post: Nov 29, 2012 1:13 AM

 Messages: [ Previous | Next ]
 Dan Christensen Posts: 8,219 Registered: 7/9/08
Re: PREDICATE CALCULUS 2
Posted: Nov 28, 2012 11:16 PM

On Nov 28, 8:59 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> On Nov 29, 8:42 am, Dan Christensen <Dan_Christen...@sympatico.ca>
> wrote:
>

> > > PROLOG is just the UNIFY( f1(..) , f1(...) )
>
> > I would love to be proven wrong, but I don't think you will get very
> > far in abstract mathematics using only PROLOG. If you are still
> > determined to used PROLOG, you might look at Norm Megill's MetaMath
> > program -- the gold standard of mechanized rigour IMHO. It is very
> > small program and, as I understand, is based entirely on making
> > not individual objects. Just maybe you can implement it in PROLOG.
> > Write to Norm. He will be able to advise you. He probably knows PROLOG
> > as well.

>
> Right, metamath uses Reverse Polish Notation
>
> 7 , 3 +
> -------
> 10
>
> and you guessed it - UNIFY() to do the matching.
>
> ...
>
> RPN is equivalent to
>
> A & B -> C
>
> that is why my Inference Rules
> (and PROLOG CLAUSES themselves)
>
> are of this form:
>
> OR
>
> if( and(X      , Y      ),    or(X,Y)       ).
> if( and(not(X) , not(Y) ),    not(or(X,Y))  ).
> if( and(not(X) , Y      ),    or(X,Y)       ).
> if( and(X      , not(Y) ),    or(X,Y)       ).
>
> TRANSITIVE IMPLICATION
>
> if( and(if(A,B) , if(B,C)),   if(A,C)       ).
>
> TRANSIVITIVE LESS THAN
>
> if( and(less(X,Y) , less(Y,Z)) ,    less(X,Z) ).
>
> etc. etc.  Similar to Metamath RPN format and PROLOG CLAUSE format,
> same matching technique too.
>
> But the advantage of using PROLOG is it is built for BACKWARD
> CHAINING.
>
> MetaMath and DCProof are 'Natural Deduction' Logics - the Human writes
> the proof!
>

I'm not sure what all that means or how it is relevant, but why don't
we just try that simple theorem again: {(x,y) | x in S, y=x} is a
function mapping the set S onto itself -- not just some particular set
of names or whatever, but ANY set S, be it finite, infinite or empty.
It's true in every case. Run it through your program and post the
automatically generated proof here -- one without any quantifiers
whatsoever.

While you are at it, let's see its proof of the non-existence of {x |
~x in x} and {x | x=x}.

What? It'll be a few more weeks? Take your time, Herc.

Dan

Date Subject Author
11/25/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Virgil
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/29/12 Graham Cooper
11/29/12 Dan Christensen
11/28/12 Frederick Williams
11/28/12 Dan Christensen
11/28/12 Dan Christensen