We present a collection of simple but powerful techniques for enhancing the efficiency of model-generation theorem provers such as Satchmo. The central ideas are to compile a clausal first order theory into a procedural Prolog program and to avoid redundant work of a naïve implementation. We also give an efficient implementation for complement splitting, a method for minimizing the first generated model and for pruning the search space. Furthermore we show that it is not efficient to ensure fair selection of clauses by a purely breadth-first search strategy and present a significantly more efficient strategy.
We have compared various combinations of our techniques among each other and with the theorem provers MGTP/G, Otter, and SETHEO, using the TPTP Problem Library as a benchmark. Our implementation has turned out to be the most efficient for range-restricted problems and for a class of problems we call “non-nesting”.