---
title: "SCOTT: A Model-Guided Theorem Prover"
authors:
  - "John K. Slaney"
doi: ""
url: "https://ijcai.org/proceedings/1993/16"
pdf: "https://ijcai.org/proceedings/1993/0016.pdf"
venue: "Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence"
year: 1993
pages: "109-114"
track: "Automated Reasoning"
keywords:
---

# SCOTT: A Model-Guided Theorem Prover

John K. Slaney

*Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence*, pages 109-114.

## 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.