Symbolic Visualization

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. We introduce 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 views of both visualizations of, and the actual outputs produced by theorem provers.

System Overview

Movie: An overview of our system (avi, 229Mb)

System overview diagram

Proof Tree Visualization

There is a lot of information that can be clearly presented to the user through the visualization of proof trees. While the structure of the overall proof will be clear in the tree structure, visual cues are used to present interesting details.

This is a proof related to a Java Virtual Machine. The image links to higher resolution version.

Sample clip from proof tree visualization (avi, 3.8Mb)

ACL2 has a model in which the subgoals can be reduced using generalization, induction, simplification etc. These actions are limited and distinct. The action taken by the theorem prover at any subgoal can be visualized by the corresponding node's color.
ACL2 provides the user with a set of statements indicating its reasoning at each subgoal. This text can be parsed and stored at each node of the proof tree to be accessed by the user.
The subgoal expressions at a node are later used for expression visualization, but are also stored at this level. Textual and graphical multi-view visualization provides details through the text, and overall structure through the graphics at the same time.
As the theorem prover proceeds, we have a set of nodes that were generated, a set of nodes that were proved, and possibly a node that could not be proved. Such information can be dynamically stored at the links by coloring them appropriately.

Multi-view text and graphical visualization of a proof attempt. The text windows on the right contain the contents of some nodes from the proof tree on the left. The screen shot is from the proof of the proposition that the reverse of the reverse of a list is the list itself (given certain conditions and definitions).

The image on the left links to a higher resolution version.

Expression Visualization

The main hurdle in finding out why the theorem prover could not prove a theorem is understanding the critical node at which the theorem prover failed or deviated from the expected path. The expression trees of formulas at a subnode can be visualized as a 2D tree. In theorem proving, larger proof attempts are cumbersome to follow. From one goal to another, the theorem prover performs some actions, modifying the expressions at each stage. In order to follow changes, pattern matching can be applied to the expressions (after suitably representing them as trees). Our heuristics for matching are domain specific. A Lisp expression E can be represented as a function symbol F operating on a set of parameters p1, p2, ... , pn. In a binary tree representation, the left child of the root node contains the function symbol F. The parameters are then the left children of all the nodes of the right side path from the root to a leaf. Two trees which have different function symbols result in a low match. The match is also proportional to the distance from the root of the differences between the trees. A permutation in the parameters of a function symbol results in a high match.

Pattern matching in expression visualization has been implemented in both text and graphics. In the figure above, we see two sets of texts (in the middle and right column). One sub-expression in the middle expression was matched with the entire expression on the right. The values returned by the our pattern matching algorithm were used to color the text. The text color gives us an estimate of pattern matching between them. Light grey font represents unselected text and black represents selected text. Once matching is performed, the black text is then augmented with colors, varying from bright to dark red, indicating high to low matches.

The results from the pattern matching are also shown with the synchronized graphical expression viewer. The result is shown in the column on the left. Grey represents unselected parts of the tree and cyan represents the selected portion. The selected expression in the top tree in the left column was searched for in the selected part of the middle tree. Again, bright to dark red is used to show high to low matches between the patterns. The third image in the left column is a zoomed in view of the outlined box in the second tree.

Publications

C. Bajaj, S. Khandelwal, J Moore, V. Siddavanahalli
Interactive Symbolic Visualization of Semi-automatic Theorem Proving
Technical Report TR-03-37, Department of Computer Sciences, University of Texas at Austin, August 2003 (pdf)

C. Bajaj, S. Khandelwal, J Moore, V. Siddavanahalli
Interactive Poster: Interactive Symbolic Visualization of Semi-automatic Theorem Proving
IEEE Symposium on Information Visualization 2003. Seattle, WA. (pdf)

Project Participants

Chandrajit Bajaj, Shashank Khandelwal, J Moore, and Vinay Siddavanahalli

This page maintained by: Shashank Khandelwal. Last updated: Wed Dec 3 11:20:48 CST 2003