Skip to main content
Journal cover image

The use of lemmas in the Model Elimination procedure

Publication ,  Journal Article
Astrachan, OL; Loveland, DW
Published in: Journal of Automated Reasoning
January 1, 1997

When the model elimination (ME) procedure was first proposed, the notion of lemma was put forth as a promising augmentation to the basic complete proof procedure. Here the lemmas that are used are also discovered by the procedure in the same proof run. Several implementations of ME now exist, but only a 1970s implementation explicitly examined this lemma mechanism, with indifferent results. We report on the successful use of lemmas using the METEOR implementation of ME. Not only does the lemma device permit METEOR to obtain proofs not otherwise obtainable by METEOR, or any other ME prover not using lemmas, but some well-known challenge problems are solved. We discuss several of these more difficult problems, including two challenge problems for uniform general-purpose provers, where METEOR was first in obtaining the proof. The problems are not selected simply to show off the lemma device, but rather to understand it better. Thus, we choose problems with widely different characteristics, including one where very few lemmas are created automatically, the opposite of normal behavior. This selection points out the potential of, and the problems with, lemma use. The biggest problem normally is the selection of appropriate lemmas to retain from the large number generated. © 1997 Kluwer Academic Publishers.

Duke Scholars

Published In

Journal of Automated Reasoning

DOI

ISSN

0168-7433

Publication Date

January 1, 1997

Volume

19

Issue

1

Start / End Page

117 / 141

Related Subject Headings

  • Computation Theory & Mathematics
  • 4613 Theory of computation
  • 4612 Software engineering
  • 4602 Artificial intelligence
  • 1702 Cognitive Sciences
  • 0802 Computation Theory and Mathematics
  • 0801 Artificial Intelligence and Image Processing
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Astrachan, O. L., & Loveland, D. W. (1997). The use of lemmas in the Model Elimination procedure. Journal of Automated Reasoning, 19(1), 117–141. https://doi.org/10.1023/A:1005770705587
Astrachan, O. L., and D. W. Loveland. “The use of lemmas in the Model Elimination procedure.” Journal of Automated Reasoning 19, no. 1 (January 1, 1997): 117–41. https://doi.org/10.1023/A:1005770705587.
Astrachan OL, Loveland DW. The use of lemmas in the Model Elimination procedure. Journal of Automated Reasoning. 1997 Jan 1;19(1):117–41.
Astrachan, O. L., and D. W. Loveland. “The use of lemmas in the Model Elimination procedure.” Journal of Automated Reasoning, vol. 19, no. 1, Jan. 1997, pp. 117–41. Scopus, doi:10.1023/A:1005770705587.
Astrachan OL, Loveland DW. The use of lemmas in the Model Elimination procedure. Journal of Automated Reasoning. 1997 Jan 1;19(1):117–141.
Journal cover image

Published In

Journal of Automated Reasoning

DOI

ISSN

0168-7433

Publication Date

January 1, 1997

Volume

19

Issue

1

Start / End Page

117 / 141

Related Subject Headings

  • Computation Theory & Mathematics
  • 4613 Theory of computation
  • 4612 Software engineering
  • 4602 Artificial intelligence
  • 1702 Cognitive Sciences
  • 0802 Computation Theory and Mathematics
  • 0801 Artificial Intelligence and Image Processing