Investigations in Model Elimination Based Theorem Proving
L O Astrachan · 1992
Automated reasoning systems, also called automatic theorem provers, have been a focus of study since computer science expanded to include the study of symbolic computation in the 1950''s. More recently, the so-called ``logic programming'''' language Prolog has been the focus of much study that has generated very efficient implementations of a language once noted for its expressive power, but now noted for its performance as well. The joining of Prolog technology with an early system of inference called Model Elimination led to the development of theorem proving systems with a very high rate of inference. This dissertation focuses on the study of automated reasoning based on Model Elimination. A theorem proving architecture and system called {\small \sl METEOR} is described and is implemented that is the foundation of a reasoning system that runs on sequential computers, NUMA shared-memory MIMD computers, and in a message-passing distributed computing environment; this reasoning system has the highest rate of inference in the world. As is well-known, brute-force is sometimes useful but must be augmented by intelligent search in many situations. We augment the search mechanism using two methods called {\em caching} and {\em lemmaizing} which lead to performance gains of more than an order of magnitude and which permit proofs to be found heretofore unobtainable by provers based on Model Elimination and by any general purpose theorem prover. We also develop different depth measures used in iterative deepening search and classes of theorems useful in the analytic study of these measures that show that no measure is uniformly superior to the other. {\small \sl METEOR} demonstrates that the high inference rate associated with Model Elimination theorem proving can be combined with redundancy reducing mechanisms and large inference steps in the form of lemmas in a powerful automated reasoning system.