System Description: SCOTT-5
Date
2001
Authors
Hodgson, K.
Slaney, John K
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
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.
Description
Keywords
Keywords: Experimental evidence; Finite domain constraints; First order; Guidance strategy; System description; Theorem provers; Artificial intelligence; Semantics
Citation
Collections
Source
Automated Reasoning: First International Joint Conference IJCAR 2001
Type
Conference paper