Advanced Proof Viewing in ProofTool

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.