SCOTT: Semantically Constrained Otter

John Slaney, Arnold Binas, Kahlil Hodgson and David Price

The SCOTT project dates back to 1991 and is still running. The theorem prover, a variant of OTTER, has competed in CASC for several years, achieving unspectacular but interesting results. It is widely regarded as an idea that ought to work but has not yet realised its potential.

The program is freely available. Like anything free, it comes with no guarantee. Unlike some free things, it also comes with no documentation: it remains very much work in progress and should be regarded as experimental software. There are several publications on SCOTT, listed below.

Son of SCOTT

This is the abstract of the paper:

John Slaney, Arnold Binas and David Price.
Guiding a Theorem Prover with Soft Constraints
Proceedings of 16th ECAI (2004): 221-225.

Attempts to use finite models to guide the search for proofs by resolution and the like in first order logic all suffer from the need to trade off the expense of generating and maintaining models against the improvement in quality of guidance as investment in the semantic aspect of reasoning is increased. Previous attempts to resolve this tradeoff have resulted either in poor selection of models, or in fragility as the search becomes over-sensitive to the order of clauses, or in extreme slowness. Here we present a fresh approach, whereby most of the clauses for which a model is sought are treated as soft constraints. The result is a partial model of all of the clauses rather than an exact model of only a subset of them. This allows our system to combine the speed of maintaining just a single model with the robustness previously requiring multiple models. We present experimental evidence of benefits over a range of first order problem domains.

The Development of SCOTT

This is the abstract of the paper:

Kahlil Hodgson and John Slaney.
TPTP, CASC and the Development of a Semantically Guided Theorem Prover.
AI Communications 15 (2002): 135-146.

The first-order theorem prover SCOTT has been through a series of versions over some ten years. The successive provers, while retaining the same underlying technology, have used radically different algorithms and shown wide differences of behaviour. The development process has depended heavily on experiments with problems from the TPTP library and has been sharpened by participation in CASC each year since 1997. In the present paper, we outline some of the difficulties inherent in designing and refining a theorem prover as complex as SCOTT, and explain our experimental methodology. While SCOTT is not one of the systems which have been highly optimised for CASC, it does help to illustrate the influence of both CASC and the TPTP library on contemporary theorem proving research.

System Description: SCOTT-5

This is the abstract of the paper:

Kahlil Hodgson and John Slaney.
System Description: SCOTT-5.
Proceedings of the First International Joint Conference on Automated Reasoning (2000): 443-446.

This paper reports recent experimental work in the development and refinement of the first order theorem prover Scott-5. This is descended from the Scott (Semantically Constrained Otter) prover (see Proc. IJCAI 1993, pp. 109-114) and uses the same combination of a saturation-based theorem prover and a finite domain constraint solver, but the architecture of Scott-5 is radically different from that of its ancestor. Here we briefly outline semantic guidance as it occurs in Scott-5, and give experimental evidence of an improvement in performance (in terms of efficiency) that we attribute to the guidance strategy.

The only famous novelist named after a theorem prover
The only famous country named after a theorem prover
The only famous polar expedition led by a theorem prover
The only famous monument to a theorem prover
Californians race to Chicago to see it in action.

Incompleteness theorem

This is the abstract of the paper:

John Slaney and Timothy J. Surendonk.
Combining Model Generation with Theorem Proving: Problems and Prospects.
Proceedings of the First International Workshop on Frontiers of Combining Systems (FrOCoS) (1996): 141-155

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.

System Description: SCOTT-1

This is the introduction to the paper:

John Slaney, Ewing Lusk and William McCune.
SCOTT, Semantically Constrained Otter: System Description.
Proceedings of the twelfth Conference on Automated Deduction (CADE-12) (1994): 798-801.

The theorem prover SCOTT, early work on which was reported in [SCOTT: A Model-Guided 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 Model-Guided Theorem Prover

This is the abstract of the paper:

John Slaney.
SCOTT: A Model-Guided Theorem Prover.
Proceedings of the thirteenth International Joint Conference on Artificial Intelligence (IJCAI-13) (1993): 109-114.

SCOTT (Semantically Constrained Otter) is a resolution-based 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
Computer Sciences Laboratory
Research School of Information Sciences and Engineering
Australian National University