SCOTT: Semantically Constrained OtterJohn Slaney, Arnold Binas, Kahlil Hodgson and David Price
This is the abstract of the paper: John Slaney and Timothy J. Surendonk. 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.
This is the introduction to the paper: John Slaney, Ewing Lusk and William McCune. The theorem prover SCOTT, early work on which was reported in [SCOTT: A ModelGuided Theorem Prover, Proc. IJCAI'93], is the result of tying together the existing prover OTTER and the existing model generator FINDER to make a new system of significantly greater power than either of its parents. The functionality of SCOTT is broadly similar to that of OTTER, but its behaviour is sufficiently different that we regard it as a separate system.
SCOTT: A ModelGuided Theorem Prover This is the abstract of the paper: John Slaney. SCOTT (Semantically Constrained Otter) is a resolutionbased 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 the 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.
Automated Reasoning Group
