Writing Programs That Construct Proofs
Journal of Automated Reasoning
When we learn mathematics, we learn more than definitions and theorems. We learn techniques of proof. In this paper, we describe a particular way to express these techniques and incorporate them into formal theories and into computer systems used to build such theories. We illustrate the methods as they were applied in the Nuprl system, essentially using the ML programming language from Edinburgh LCF as the formalized metalanguage. We report our experience with such an approach emphasizing the ideas that go beyond the LCF work, such as the transformation tactics and special purpose reasoners. We also show how the validity of tactics can be guaranteed. The introduction places the work in historical context and the conclustion briefly describes plans to carry the methods further. The majority of the paper presents the Nuprl approach in detail.
bibTex ref: CKB84