On the implementation of an extensible declarative proof language?

Abstract

Following the success of the Mizar [15, 9] system in the mechanisation of mathematics, there is an increasing interest in the theorem proving community in developing similar declarative languages. In this paper we discuss the implementation of a simple declarative proof language (SPL) on top of the HOL system where scripts in this language are used to generate HOL theorems, and HOL 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 mechanisation of a theory. A case study in the mechanisation of group theory illustrates how this extensibility can be used to reduce the difierence between formal and informal proofs, and therefore increase the readability of formal proofs.