mramesh@cbnewse.ATT.COM (m.ramesh) (03/27/90)
I have just started using prolog (Turbo Prolog) on PC and I do like it. I believe it does theorem proving. Is it possible to prove geometry theorems using prolog. For eg., given that B is a mid-point of line AC, prove that AB=AC/2, is it possible to write a program in prolog to do such proofs, with a given set of postulates. I might have mis-understood the meaning of theorem proving in prolog but I feel it can be done. Can someone help me out on this. Thanks *** Ramesh, AT&T Bell Labs, Naperville, IL
feldman@Neon.Stanford.EDU (Todd J. Feldman) (03/28/90)
In article <13843@cbnewse.ATT.COM> mramesh@cbnewse.ATT.COM (m.ramesh) writes: >I have just started using prolog (Turbo Prolog) on PC and I do like it. >I believe it does theorem proving. Is it possible to prove geometry >theorems using prolog. For eg., given that B is a mid-point of line AC, >prove that AB=AC/2, is it possible to write a program in prolog to do >such proofs, with a given set of postulates. You can prove such theorems, provided they are defined in the proper theory with the proper axioms defined. For example, I have written a theorem prover in Prolog using the deductive techniques of Manna and Waldinger. Of course, you can't just give Prolog a theorem and say "prove me;" you need to define the mechanisms by which the proof is carried out. There a skillion (somewhere between a million and a billion) ways to implement this. Prolog is very useful for theorem proving, based on its inherent logical framework.