METEOR - EXPLORING MODEL ELIMINATION THEOREM-PROVING

In this paper we describe the theorem prover METEOR which is a high-performance model elimination prover running in sequential, parallel, and distributed computing environments. METEOR has a very high inference rate. But, as is the case with better chess-playing programs, speed alone is not sufficient when exploring large search spaces; intelligent search is necessary. We describe modifications to traditional iterative deepening search mechanisms whose implementation in METEOR result in performance improvements of several orders of magnitude and that have permitted the discovery of proofs unobtainable by top-down model elimination provers.