Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

Publication Details

Caching and Lemmaizing In Model Elimination Theorem Provers

by Astrachan, Owen L. and Stickel, Mark E.

Technical Note 513
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave., Menlo Park, CA 94025
Dec 1991.

Order an AIC Technical Note

Abstract

Theorem provers based on the model elimination theorem-proving procedure have exhibited extremely high inference 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.

Electronic Copies


Adobe PDF

BibTeX

EndNote

AIC Personnel

Name Title E-mail
Stickel, Mark E Principal Scientist

SRI International
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy