METEOR (original) (raw)

METEOR is a theorem prover based on Model Elimination. It runs on Unix machines and networks of Unix machines (and used to run on the BBN Butterfly TC2000)

There are several papers describing METEOR, theoretical and empirical results, and modifications to the search mechanism

• Caching and Lemmaizing in Model Elimination Theorem Provers with Mark Stickel. Available as SRI International Technical Note 513, December 1991. Shorter version appeared in CADE-11, available via ftp.
• Investigations in Model Elimination Based Theorem Proving (Ph.D. thesis, 1992) available via ftp
• The Use of Lemmas in the Model Elimination Procedure with Donald Loveland, Duke Technical Report CS-1993-25 available via ftp
• METEOR: Exploring Model Elimination Theorem Proving. Journal of Automated Reasoning, v. 13, 1994, pages 283-296. Available (as techreport) via ftp
• The Use of Lemmas in the Model Elimination Procedure with D.W. Loveland, to appear in Journal of Automated Reasoning. This is an updated version of a previous report.