SCOTT: A Model-Guided Theorem Prover
Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. 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.
@inproceedings{ijcai1993p16,
title = {SCOTT: A Model-Guided Theorem Prover},
author = {Slaney, John K.},
booktitle = {Proceedings of the Thirteenth International Joint Conference on
Artificial Intelligence, {IJCAI-93}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Ruzena Bajcsy},
pages = {109--114},
year = {1993},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1993/16},
}
TY - CPAPER TI - SCOTT: A Model-Guided Theorem Prover AU - Slaney, John K. T2 - Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, IJCAI-93 PB - International Joint Conferences on Artificial Intelligence PY - 1993 SP - 109 EP - 114 UR - https://ijcai.org/proceedings/1993/16 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
