SCOTT: A Model-Guided Theorem Prover

Abstract

SCOTT (Semantically Constrained Otter) is a resolution-based automatic theorem prover for first order logic. It is based on the high performance prover OTTER by W. McCune and also incorporates a model generator. This finds finite models which SCOTT is able to use in a variety of ways to direct its proof search. Clauses generated by the prover are in turn used as axioms of theories to be modelled. Thus prover and model generator inform each other dynamically. This paper describes the algorithm and some sample results. SCOTT (Semantically Constrained Otter) is a resolution based automatic theorem prover for first order logic. So much is hardly revolutionary. What is new in SCOTT is the way in which it blends traditional theorem proving methods, best seen as purely syntactic, with techniques for semantic investigation more usually associated with constraint satisfaction problems. Thus it bridges two aspects of the science of reasoning. It was made by marrying an existing high-...