Abstract
For several decades, there has been significant debate over the formal proof style supported by proof assistants. For example, the merits of a declarative style rather than a procedural (tactic) style have been argued. In much of the debate, there has been unnecessarily rigid insistence on the languages of proof input and proof presentation being identified. When these concepts are not shackled together, many opportunities are opened up for dynamic proof presentation that take full advantage of the capabilities of computer user interfaces. With dynamic proof presentation, the proof viewer can easily focus attention on particular parts of proofs and change the level of detail presented. One viewer might be interested in just a proof outline, another might want to see how a large step of inference is composed of smaller steps. Current proof assistant user interfaces do provide some dynamic presentation capabilities, but much more could be done. Further attention to dynamic proof presentation should help make formal proofs easier to understand by a wider range of audiences, with minimal need to rewrite proof libraries that are developed with huge time investments.
| Original language | English |
|---|---|
| Title of host publication | Mathematical Reasoning: The History and Impact of the DReaM Group |
| Editors | Gregory Michaelson |
| Place of Publication | Cham |
| Publisher | Springer International Publishing |
| Chapter | 4 |
| Pages | 63-86 |
| Number of pages | 24 |
| ISBN (Electronic) | 978-3-030-77879-8 |
| ISBN (Print) | 978-3-030-77878-1, 978-3-030-77881-1 |
| DOIs | |
| Publication status | Published - 24 May 2021 |