Path: utzoo!utgpu!news-server.csri.toronto.edu!clyde.concordia.ca!uunet!snorkelwacker!usc!elroy.jpl.nasa.gov!decwrl!shelby!neon!feldman
From: feldman@Neon.Stanford.EDU (Todd J. Feldman)
Newsgroups: comp.lang.prolog
Subject: Re: prolog theorem proving
Message-ID: <1990Mar28.022843.12017@Neon.Stanford.EDU>
Date: 28 Mar 90 02:28:43 GMT
References: <13843@cbnewse.ATT.COM>
Distribution: na
Organization: Computer Science Department, Stanford University
Lines: 14

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.