Multi-threading in an interactive theorem prover
Phil Cook, Peter Robinson · 1999
s and compressed postscript files are available via http://svrc.it.uq.edu.au Multi-threading in an Interactive Theorem Prover Phil Cook Peter Robinson Abstract The Ergo theorem prover is an interactive prover that is currently being used by the SVRC for carrying out proofs associated with the development of trusted software. The current version of Ergo is a single-threaded prover. A multi-threaded version would allow many possibilities for improving the effectiveness of the prover. For example, automatic tactics for simple sub-proofs and rule browsers could be run as background threads while the user is planning and carrying out more complex proof tasks. This paper describes some strategies for constructing a multithreaded prover using the high-level communication and thread facilities found in Qu-Prolog 5.0. 1 Introduction The Ergo theorem prover [1] is an interactive prover, developed by the Software Verification Research Centre, used to perform proofs associated with t...