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