document: TPTP , CASC and the development of a semantically guided theorem prover The first-order theorem prover SCOTT has been through a series of versions over some ten years . The successive provers , while retaining the same underlying technology , have used radically different algorithms and shown wide differences of behaviour . The development process has depended heavily on experiments with problems from the TPTP library and has been sharpened by participation in CASC each year since 1997 . We outline some of the difficulties inherent in designing and refining a theorem prover as complex as SCOTT , and explain our experimental methodology . While SCOTT is not one of the systems which have been highly optimised for CASC , it does help to illustrate the influence of both CASC and the TPTP library on contemporary theorem proving research
doc_bio_tags: O O B O O O O O B I I I O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B I O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O B O O O O B I O O B O O O O O O O O O O O O B O O O O O O O O O O B O O B I O O O O O