Summary: Caching and Lemmaizing in Model Elimination
Owen L. Astrachan
Department of Computer Science
Durham, NC 27706
Mark E. Stickel
Artificial Intelligence Center
Menlo Park, CA. 94025
Theorem provers based on model elimination have exhibited extremely high in-
ference rates but have lacked a redundancy control mechanism such as subsumption.
In this paper we report on work done to modify a model elimination theorem prover
using two techniques, caching and lemmaizing, that have reduced by more than an
order of magnitude the time required to find proofs of several problems and that
have enabled the prover to prove theorems previously unobtainable by top-down
model elimination theorem provers.