Structured Presentation of Formal Proofs: an Experiment with Isabelle

The intelligible presentation of formal proofs is usually not attempted because of their technical detail. This formal noise hides the line of reasoning that can be followed and understood by humans. We are investigating methodologies and machine support for presenting formal proofs in an intelligible and structured manner while keeping them amenable to a check by a machine or an interactive development. To this end, we have in the past carried out sizable experiments with an implementation of the logical framework Deva, a descendant of the AUTOMATH family of languages [WSL93, SBR94, AJS94, Web94]. The experiments were carried out in the context of formal software development as well as mathematical proofs. Although Deva served its purpose as an experimental prototype very well, it turned out to be, in the long run, too monolithic and inflexible (for instance, the module mechanism was internalized into the meta-logic). Still, we think that the various concepts that underlie the specific approach we chose for the presentation of formal proofs in Deva are of a general nature. We are currently trying to apply this approach to proofs expressed in other logical frameworks, Isabelle in particular, and we continue to investigate theoretical aspects of expressing formal proofs. More specifically: