zbMATH — the first resource for mathematics

Nuprl as a concurrent interactive theorem prover. (English) Zbl 0884.68114
Dean, Nathaniel (ed.), African Americans in mathematics. Proceedings of the second conference for African-American researchers in the mathematical sciences held at DIMACS, Piscataway, NJ, USA, June 26–28, 1996. Providence, RI: American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 34, 149-154 (1997).
Summary: We describe how to redesign the Nuprl proof developement system in order to perform concurrent inference. We focus on the design of the inference engine of Nuprl, the refiner. Our design consists of making the refiner a multithreaded program in which each thread behaves as a refiner. With the multithreaded refiner, we are able to develop tactics that execute concurrently. Tactics are programs employed by users to construct proofs within Nuprl. By having them execute concurrently, Nuprl will be the first interactive theorem prover with concurrent inference.
For the entire collection see [Zbl 0872.00023].
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Nuprl; Refiner