Skip to main content
Journal cover image

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

Altmetric Attention Stats
Dimensions Citation Stats

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

ISBN

9783540556022

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.
Journal cover image

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

ISBN

9783540556022

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