Combining finite model generation with theorem proving - Problems and prospects

This paper is about automatic searching for proofs, automatic searching for models and the potentially fruitful ways in which these traditionally separate aspects of reasoning may be made to interact. It takes its starting point in research reported in 1993 (Slaney, SCOTT: A Semantically Guided Theorem Prover, Proc. 13th IJCAI) on a system which combines a high performance first order theorem prover with a program generating small models of first order theories. The main theorem is an incompleteness result for a certain range of problems to which this combined system has been successfully applied. While the result may not be unexpected, the proof is worth examining and it is important to reflect on its relationship to the research program in combining methods.