 |
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.
|
-
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.
|
Downloads
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)
Related Links
|
ACL2 (Our case study theorem prover)
|
|
CCV (Center for Computational Visualization)
|
Project Participants
Chandrajit Bajaj, J Moore, and Vinay Siddavanahalli
Research supported in part by grants from NSF CCR-9988357and ACI 9982297
|
|
