PROOFTOOL: a GUI for the GAPT Framework

10th International Workshop On User Interfaces for Theorem Provers, UITP 2012
Bremen, Germany


This paper describes an implementation and the features of a proof viewer which fulfills the role of a graphical user interface to the General Architecture for Proof Theory (GAPT) framework. It contains methods to render classical and schematic sequent calculus proofs as well as resolution proofs and other tree-like structures in a flexible way. Additional emphasis is put on the schema proof input format for the end-user which should be as user-friendly as possible.