Visualising First-Order Proof Search

Graham Steel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 2005 Workshop on User Interfaces for Theorem Provers (UITP '05)
Pages179-189
Number of pages11
Publication statusPublished - 2005

Cite this