Handbook of Automated Reasoning

7 Architectures of Model Elimination Implementations

All competitive implementations of model elimination are iterative-deepening search procedures using backtracking. When envisaging the implementation of such a procedure, one has the choice between fundamentally different architectures, for reasons we will now explain. As indicated at the end of Section 2.7.1, it is straightforward to recognize that SLD-resolution (the inference system underlying Prolog) can be considered as a refinement of model elimination obtained by simply omitting the reduction inference rule. Since highly efficient implementation techniques for Prolog have been developed, one can profit from these efforts and design a Prolog Technology Theorem Prover (PTTP). The crucial ...