gio@crcc.UUCP (Giordano Pezzoli) (11/18/88)
Hi, I'm finding reference, hint, source about resolution in Prolog. I'm trying to build a complete resolutor, that is a first order language interpreter that translate axioms and thesis in clause form; then apply a resolution method to prove the thesis from axioms. Any suggestion is welcome, Gio` +-----------------------------------------------------------------------+ | UUCP: ...!mcvax!i2unix!crcc!gio ***** * | | Pezzoli Giordano * \ | | CRCC Informatica s.r.l. * ** * *** \ | | via Passerini 2, 20052 Monza (ITALY). * * * * * | | Phone: 039-387998. ***** * *** | +-----------------------------------------------------------------------+
ok@quintus.uucp (Richard A. O'Keefe) (11/20/88)
In article <436@crcc.UUCP> gio@crcc.UUCP (Giordano Pezzoli) writes: >I'm finding reference, hint, source about resolution in Prolog. You might like to look at the book The Computer Modelling of Mathematical Reasoning by Alan Bundy; 1983; Academic Press; ISBN 0-12-141352-0
ke@otter.hpl.hp.com (Kave Eshghi) (12/10/88)
You might benefit from looking at the following paper: A Prolog Technology Theorem Prover by Marc Stickle. It is published in the proceedings of Conference on Automated Deduction (1986) Marc Stickle is at SRI International. Have Fun Kave Eshghi