@inproceedings{d5269fd82f97400dacffba569ce7c984,
title = "System description: SCOTT-5",
abstract = "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.",
author = "Kahlil Hodgson and John Slaney",
year = "2001",
doi = "10.1007/3-540-45744-5_36",
language = "English",
isbn = "3540422544",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "443--447",
editor = "Rajeev Gore and Alexander Leitsch and Tobias Nipkow",
booktitle = "Automated Reasoning - First International Joint Conference, IJCAR 2001, Proceedings",
address = "Germany",
note = "1st International Joint Conference on Automated Reasoning, IJCAR 2001 ; Conference date: 18-06-2001 Through 22-06-2001",
}