System Description: SCOTT-5
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Automated Reasoning: First International Joint Conference IJCAR 2001|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.