Abstract

Interactive Poster: Interactive Symbolic Visualization of Semi-automatic Theorem Proving

We present an interactive visualization environment for semi-automatic theorem provers in an attempt to help users better steer their theorem proving process. The augmented theorem proving environment provides synchronized multi-resolution textural 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 textual and graphical visualizations enhance user understanding.