d83_sven_a@tekno.chalmers.se (SVEN AXELSSON) (02/17/90)
I'm currently doing research on computational discourse semantics and I wonder if anybody has a theorem prover, written in Prolog, to share with me. It should (of course) be for a logic more expressive than horn clause logic, and as I want to be able to follow the structure of the proofs, preferably a non-resolution method should be used (a tableaux method, for example). Programs and/or advices and/or pointers to relevant literature are most welcome. Thanks for your help. Torbjoern Lager E-mail: lager@hum.gu.se Department of Philosopy S-412 98 Gothenburg Sweden
ranga@uceng.UC.EDU (Dr. Ranga R. Vemuri) (02/26/91)
I have heard that someone implemented a theorem prover in Prolog based on the Boyer-Moore computational logic. Can anyone please give me pointers to this. Also, are there any public domain (or available at no cost..) theorem provers (propositional or first-order or higher-order) implemented in Prolog. Thanks for the info. - ranga ranga@uceng.uc.edu ______________
geraint@aipna.ed.ac.uk (Geraint Wiggins) (02/28/91)
We have a Prolog based theorem prover called Oyster which we use for our proof planning research work. It is a reimplementation of Constable et al's NUPRL system in prolog by Christian Horn. It works in Martin-Lof Constructive Type Theory and is able to extract programs from proofs developed in it. We distribute Oyster at media cost, along with the current version of the CLaM proof planner. We are currently working on a version of the system working in 1st order sorted logic. Contact Gordon Reid (gordon@uk.ac.ed.ai) for further details. Hope this helps. Geraint