Exploiting parallelism in interactive theorem provers

This paper reports on the implementation and analysis of the MP refiner, the first parallel interactive theorem prover. The MP refiner is a shared memory multi-processor implementation of the inference engine of Nuprl. The inference engine of Nuprl is called the refiner. The MP refiner is a collection of threads operating as sequential refiners running on separate processors. Concurrent tactics exploit parallelism by spawning tactics to be evaluated by other refiner threads simultaneously. Tests conducted with the MP refiner running on a four processor Spare shared-memory multi-processor reveal that parallelism at the inference rule level can significantly decrease the elapsed time of constructing proofs interactively.