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)

TL;DR
This paper introduces a novel Sunburst Tree layout for proof visualization in ProofTool, enhancing understanding of sequent calculus proofs by focusing on structural content through concentric circle arcs.
Contribution
It proposes the Sunburst Tree layout as a new visualization method and evaluates its effectiveness compared to traditional tree structures.
Findings
Sunburst layout improves focus on proof structure
Evaluation shows better comprehension with Sunburst visualization
Integration into ProofTool enhances proof analysis capabilities
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
