%0 Report %@ 45R %A Brice, Claude R. and Derksen, Jan A. %T Heuristically Guided Equality Rule in a Resolution Theorem Prover %C 333 Ravenswood Ave, Menlo Park, CA 94025 %I AI Center, SRI International %D 1971 %K Theorem prover, E-Resolution, Inference %X A new way of handling the equality relation within the framework of a resolution theorem prover is described. The system uses a modification of Morris’ E-resolution, a rule of inference to handle equality, controlled by heuristic search techniques. The modification makes possible an implementation to which new rules of inference may be added easily. %O SRI Project 8259. The research reported herein was sponsored by the Advanced Research Projects Agency and the National Aeronautics and Space Administration under Contract NAS12-2221. %U http://www.ai.sri.com/pubs/files/1532.pdf
