A Proof Description Language and Its Reduction System
Masamichi Hagiya
Kyoto University, Japan
![A Proof Description Language and Its Reduction System cover](/_next/image?url=https%3A%2F%2Fcontent.ems.press%2Fassets%2Fpublic%2Fimages%2Fserial-issues%2Fcover-prims-volume-19-issue-1.png&w=3840&q=90)
Abstract
The normalization of a natural deduction proof of a closed existential formula gives a term and a proof of . This allows us to regard a proof as a program (Goad [9] [10] etc.). But it is not always necessary to completely normalize the given proof to obtain . We analyze the situation by introducing the notions called minimal -reduct, proper reduction etc.; in a word, we define the normal order of proof reduction and study its proof-theoretical property. Then, we present an experimental proof-checker-reducer system that actually uses those principles. In designing a proof-checker (or rather a proof description language), we focussed our attention on the readability of proofs.
Cite this article
Masamichi Hagiya, A Proof Description Language and Its Reduction System. Publ. Res. Inst. Math. Sci. 19 (1983), no. 1, pp. 237–261
DOI 10.2977/PRIMS/1195182986