Dynamic Proof Presentation

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

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 languageEnglish
Title of host publicationMathematical Reasoning: The History and Impact of the DReaM Group
EditorsGregory Michaelson
Place of PublicationCham
PublisherSpringer International Publishing
Chapter4
Pages63-86
Number of pages24
ISBN (Electronic)978-3-030-77879-8
ISBN (Print)978-3-030-77878-1, 978-3-030-77881-1
DOIs
Publication statusPublished - 24 May 2021

Fingerprint

Dive into the research topics of 'Dynamic Proof Presentation'. Together they form a unique fingerprint.

Cite this