METEORs: High Performance Theorem Provers using Model Elimination. It has been thought for some time that linear resolution procedures are not the best resolution formats for doing very large unguided searches such as are required for proving significant mathematical theorems. Although very efficient with storage space, the depth-first implementations that take advantage of the linearity seem to preclude use of subsumption and similar devices to reduce redundant search. However, research in logic programming has led to sophisticated architectures giving high-speed performance for Prolog, which is based on a linear input resolution procedure. In particular, the WAM architecture, due to D. H. D. Warren (see [33]) has proven very successful. This has led to renewed interest in Model Elimination (ME) ([18, 19, 20]), which is a linear input proof procedure for full first-order logic, similar to but distinct from resolution. Interest has revived because there are situations where the significantly higher inference rate may offset the removal of some redundant computations.

References in zbMATH (referenced in 16 articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
  2. Otten, Jens; Bibel, Wolfgang: IeanCOP: lean connection-based theorem proving (2003)
  3. Bonacina, Maria Paola; Hsiang, Jieh: On the modelling of search in theorem proving -- towards a theory of strategy analysis (1998)
  4. Bonacina, Maria Paola; Hsiang, Jieh: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. (1998) ioport
  5. Bonacina, Maria Paola; Hsiang, Jieh: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. (1998) ioport
  6. Horton, J. D.; Spencer, Bruce: Clause trees: A tool for understanding and implementing resolution in automated reasoning (1997)
  7. Iwanuma, Koji: Lemma matching for a PTTP-based top-down theorem prover (1997)
  8. Reed, David W.; Loveland, Donald W.: Near-Horn Prolog and the ancestry family of procedures (1995)
  9. Astrachan, Owen: METEOR: Exploring model elimination theorem proving (1994) ioport
  10. Bonacina, Maria Paola; Hsiang, Jieh: Parallelization of deduction strategies: An analytical study (1994) ioport
  11. Letz, R.; Mayr, K.; Goller, C.: Controlled integration of the cut rule into connection tableau calculi (1994)
  12. Schumann, J.: Tableau-based theorem provers: Systems and implementations (1994) ioport
  13. Sturgill, David B.; Segre, Alberto Maria: A novel asynchronous parallelism scheme for first-order logic (1994)
  14. Bledsoe, W. W.; Feng, Guohui: SET-VAR (1993)
  15. Stickel, Mark E.: A Prolog technology theorem prover: A new exposition and implementation in Prolog (1992)
  16. Boyer, Robert S. (ed.): Automated reasoning. Essays in honor of Woody Bledsoe (1991)