Instance-Based Theorem Proving with Semantics and Equality

Principal Investigator: David Plaisted
Funding Agency: National Science Foundation
Agency Number: CCR-9972118

Abstract
The ordered semantic hyper-linking strategy (OSHL) combines propositional efficiency, semantics, and equality in one integrated automatic theorem prover for first-order logic. Semantics refers to the meanings of symbols, and propositional efficiency refers to efficiency on problems requiring significant case analysis. Few existing provers utilize semantics, and most are not propositionally efficient. The current Prolog implementation will be extended in ways that were suggested by a recent paper on the topic. The prover will also be re-implemented in Scheme for greater speed. In addition, a prover combining equality, unification, and propositional efficiency but no semantics will be implemented, because semantics may not always be available. These combinations should outperform almost all other provers on a significant class of problems. Techniques capable of effective theorem proving on sets of millions of input clauses will also be sought.