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: PREDICATE CALCULUS 2
Replies: 23   Last Post: Nov 29, 2012 1:13 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,348
Registered: 5/20/10
Re: PREDICATE CALCULUS 2
Posted: Nov 28, 2012 8:59 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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
> symbolic substitutions. Your "facts" would be facts about formuala's,
> 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!

Herc




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

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.