An Exploration Tool for Formal Proofs

Proof assistants aid the user in proving mathematical theorems by taking care of low-level reasoning details. Their user interfaces often present proof information as text, which becomes increasingly dicult to compre- hend as it grows in size. Panoptes is a software tool that enables users to explore graphical representations of the formal proofs produced by the imps Interactive Mathematical Proof System. Panoptes automatically displays an imps deduction graph as a visual graph that can be easily manipulated by the user. Its facilities include target zooming, oating information boxes, node relabeling, and proper substructure collapsing.