This paper describes a method for visualising proof search in automatic resolution-style first-order theorem provers. The method has been implemented in a simple tool called viz, which takes advantage of the widely-supported scalar vector graphics format to produce graphs which can be viewed interactively. This allows the user to zoom in and out, pan, and get more information by clicking on particular parts of the graph. We demonstrate how the graphs can be used to suggest improvements to the strategy and heuristics used in the proof attempt.
|Title of host publication||Proceedings of the 2005 Workshop on User Interfaces for Theorem Provers (UITP '05)|
|Number of pages||11|
|Publication status||Published - 2005|