Heuristically Guided Equality Rule in a Resolution Theorem Prover
by Brice, Claude R. and Derksen, Jan A.
Technical Note 45R
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave, Menlo Park, CA 94025
Jan 1971.
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.
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.
 Adobe PDF |
 BibTeX |
 EndNote |
| Name | Title | ||
|---|---|---|---|
| Brice, Claude R. | Alumnus | ||
| Derksen, Jan | Alumnus |
