Abstract

Interactive Symbolic Visualization of Semi-automatic Theorem Proving

We explore a new symbolic visualization model for semi-automatic theorem provers. Mechanized formal methods are finding increased use in the design and development of complex hardware and software systems. Most proofs are presented in a textual format, with intermediate formulas possibly consisting of megabytes of data, which are difficult to analyze and understand. This paper introduces a preliminary visualization environment for semi-automatic theorem provers in an attempt to help users steer the theorem proving process. The environment provides synchronized multi-resolution textual and graphical views and direct navigation of large expressions or proof trees from either of the twin interfaces. We identify three levels of the proof process at which synchronized multi-resolution graphical and textual visualization enhance user understanding.