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)