# A Proof Description Language and Its Reduction System

### Masamichi Hagiya

Kyoto University, Japan

## Abstract

The normalization of a natural deduction proof of a closed existential formula ∃_xA_ gives a term *t* and a proof of *Ax*[*t*]. 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 *t*. We analyze the situation by introducing the notions called *minimal I-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