Advanced Proof Viewing in ProofTool

Tomer Libal
(Microsoft Research - Inria Joint Center, Ecole Polytechnique)
Martin Riener
(Institute of Computer Languages, Vienna University of Technology)
Mikheil Rukhaia
(Institute of Applied Mathematics, Tbilisi State University)

Sequent calculus is widely used for formalizing proofs. However, due to the proliferation of data, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but since they normally utilize Gentzen's original notation, some of the problems persist. In this paper, we introduce a number of criteria for proof visualization which we have found out to be crucial for analyzing proofs. We then evaluate recent developments in tree visualization with regard to these criteria and propose the Sunburst Tree layout as a complement to the traditional tree structure. This layout constructs inferences as concentric circle arcs around the root inference, allowing the user to focus on the proof's structural content. Finally, we describe its integration into ProofTool and explain how it interacts with the Gentzen layout.

In Christoph Benzmüller and Bruno Woltzenlogel Paleo: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, 17th July 2014, Electronic Proceedings in Theoretical Computer Science 167, pp. 35–47.
Published: 29th October 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: