Publication in BibTeX Format

@TECHREPORT{AICPub1532:1971,
  AUTHOR={Brice, Claude R. and Derksen, Jan A. },
  TITLE={Heuristically Guided Equality Rule in a Resolution Theorem Prover},
  ADDRESS={333 Ravenswood Ave, Menlo Park, CA 94025},
  INSTITUTION={AI Center, SRI International},
  MONTH={Jan},
  NUMBER={45R},
  YEAR={1971},
  KEYWORDS={Theorem prover, E-Resolution, Inference},
  ABSTRACT={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.},
  NOTE={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.}
}