On the implementation of an extensible declarative proof language (Q4945207)

Following the success of the Mizar system in the mechanization of mathematics, there is an increasing interest in the theorem proving community in developing similar declarative languages. In this paper the implementation of a Simple declarative Proof Language (SPL) on top of the H0L system is discussed, where scripts in this language are used to generate H0L theorems, and H0L definitions, axioms, theorems and proof procedures can be used in SPL scripts. Unlike Mizar, the language is extensible, in the sense that the user can extend the syntax and semantics of the language during the mechanization of a theory. A case study in the mechanization of group theory illustrates how this extensibility can be used to reduce the difference between formal and informal proofs, and therefore increase the readability of formal proofs. For the entire collection see [Zbl 0929.00038].