Panoptes: An Exploration Tool for Formal Proofs*

Abstract:

Proof assistants aid the user in proving mathematical theorems by taking care of low-level reasoning details. Their user interfaces often present proof information as text, which becomes increasingly difficult to comprehend as it grows in size. Panoptes is a software tool that enables users to explore graphical representations of the formal proofs produced by the IMPS Interactive Mathematical Proof System. Panoptes automatically displays an IMPS deduction graph as a visual graph that can be easily manipulated by the user. Its facilities include target zooming, floating information boxes, node relabeling, and proper substructure collapsing.

Thesis (pdf with bookmarks; high quality, suitable for printing; ~5.5 Mb): view or right-click to save. 

Thesis (pdf with bookmarks; lower quality, good for screen view ; ~1.4 Mb): view or right-click to save.

Demo movie (~140 Mb): play or right-click to save. 

Demo movie 2 (shorter, ~72 Mb): play or right-click to save. 

Source code: download.

Installation: untar the archive to a folder, then run "./install" followed by "make". Panoptes can then be started by "./panoptes". Notice that this will compile Panoptes in testing mode, and it will use the provided with the archive package sample deduction graphs. To compile for use with IMPS, the user should edit the file "panoptes.ml" by replacing the line "let testing = true" with "let testing = false" that can be found towards the beginning of the file. Furthermore, Panoptes should be started with "./panoptes" AFTER a proof in IMPS has been initiated (otherwise Panoptes will look for nonexistend IMPS files and will fail to start). After that Panoptes can be restarted when new proofs are started in IMPS by just clicking "r" on the keyboard (click "h" during runtime to get a list of all available shortcuts).

* Designed and implemented by Orlin Grigorov (supervisor: Dr. William M. Farmer). Developed in partial fulfilment of the requirements for the degree of M.Sc. in Computer Science, Department of Computing and Software, McMaster University.

Last updated: June 29, 2008