Caching and lemmaizing in model elimination theorem provers
Publication
, Conference
Astrachan, OL; Stickel, ME
Published in: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
January 1, 1992
Theorem provers based on model elimination 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.
Duke Scholars
Published In
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI
EISSN
1611-3349
ISSN
0302-9743
Publication Date
January 1, 1992
Volume
607 LNAI
Start / End Page
224 / 238
Related Subject Headings
- Artificial Intelligence & Image Processing
- 46 Information and computing sciences
Citation
APA
Chicago
ICMJE
MLA
NLM
Astrachan, O. L., & Stickel, M. E. (1992). Caching and lemmaizing in model elimination theorem provers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 607 LNAI, pp. 224–238). https://doi.org/10.1007/3-540-55602-8_168
Astrachan, O. L., and M. E. Stickel. “Caching and lemmaizing in model elimination theorem provers.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 607 LNAI:224–38, 1992. https://doi.org/10.1007/3-540-55602-8_168.
Astrachan OL, Stickel ME. Caching and lemmaizing in model elimination theorem provers. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1992. p. 224–38.
Astrachan, O. L., and M. E. Stickel. “Caching and lemmaizing in model elimination theorem provers.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 607 LNAI, 1992, pp. 224–38. Scopus, doi:10.1007/3-540-55602-8_168.
Astrachan OL, Stickel ME. Caching and lemmaizing in model elimination theorem provers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1992. p. 224–238.
Published In
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI
EISSN
1611-3349
ISSN
0302-9743
Publication Date
January 1, 1992
Volume
607 LNAI
Start / End Page
224 / 238
Related Subject Headings
- Artificial Intelligence & Image Processing
- 46 Information and computing sciences