|
|
Simons M.
(1996)
|
   |
|
|
|
|
|
|
Abstract In this thesis we present an approach to the intelligible communication of formal proofs. Observing a close correspondence between the activities of formal-proof development and program development, and using this as a guideline, we apply well-known principles from program design to proof design and presentation, resulting in formal proofs presented in a literate style, that are hierarchically structured, and that emphasize calculation. We illustrate the general practicability of this approach by describing two concrete experiments in which we instantiated it to the case of formal proofs expressed in a static proof language, and proofs programmed with an interactive theorem prover. In each case, we describe the instantiation and the tools we developed for supporting the presentation, taking into account the underlying logical framework, and then use these tools to present formal proofs of nontrivial mathematical theorems. Recognizing that two essential elements of our approach---the composition of deductions and their hierarchical refinement---are lacking in conventional proof calculi, we describe an algebraic proof calculus in which formal deductions are first-class citizens that can be composed and refined. We show that refinements are formally expressible in this framework, which in the two experiments can only be realized by extralogical means. The main achievement of the present thesis is, then, the practical evidence we obtained of the usefulness of integrating the notions of composition and refinement into logical frameworks to improve the presentation of formal proofs; the formulation of an algebraic semantics for such a framework; and the construction of techniques and tool architectures to obtain the suggested improvements in presentation using conventional frameworks.
|