Visualizing Proof Search for Theorem Prover Development
JOHN J. BYRNES, Michael Buchanan, Michael D. Ernst, Phil Miller, Chris Roberts, Robert Keller · Electronic Notes in Theoretical Computer Science · 2009
We describe an interactive visualization tool for large natural deduction proof searches. The tool permits the display of a search as it progresses, as well as the proof tree itself. We discuss the feature set and architecture of the tool, including aspects of extensibility and the interface for interaction with other user-provided analysis and visualization code.