SCOTT: Semantically Constrained Otter

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.