[comp.lang.prolog] PD FOPC Theorem Prover with equality

bond@sce.carleton.ca (Greg Bond) (05/31/90)

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