Advanced Proof Viewing in PROOFTOOL

ABSTRACT. Sequent calculus is widely used for formalizing proofs. However, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but most stick with Gentzen's original notation. This paper tries to catch up with recent developments in tree visualization and proposes the Sunburst Tree layout as a complement to the traditional tree structure. It constructs inferences as concentric circle arcs around the root inference, allowing the user to investigate the proof's structural content. We further describe the integration into PROOFTOOL and the interaction with the Gentzen layout.