Xref: utzoo comp.ai:6939 comp.lang.prolog:2751 sci.philosophy.tech:2423 sci.logic:825
Path: utzoo!dciem!nrcaer!sce!bond
From: bond@sce.carleton.ca (Greg Bond)
Newsgroups: comp.ai,comp.lang.prolog,sci.philosophy.tech,sci.logic
Subject: PD FOPC Theorem Prover with equality (repost)
Keywords: FOPC,theorem prover
Message-ID: <864@sce.carleton.ca>
Date: 31 May 90 02:28:12 GMT
Followup-To: poster
Organization: Systems & Computer Eng. Dept.,Carleton University,Ottawa,Canada
Lines: 14


I am in search of a public domain theorem prover that will efficiently
handle the equality relation for FOPC. I have a logical specification of a
problem that includes the equality relation and utilizes functional
notation.  Including the axioms of equality causes an exponential increase
in the number of useless (in terms of proving inconsistency) deductions. The
theorem prover should be complete for proving inconsistency of a set of
wffs.

-- 
------------------------------------------------------------------
Greg Bond   ----->   bond@sce.carleton.ca  (613) 788 5743
Dept. of Systems and Computer Engineering, Carleton University
Ottawa, ON, Canada K1S 5B6