The Design and Implementation of an Interactive Proof Editor
Abstract
This thesis describes the design and implementation of the IPE, an interactive
proof editor for first-order intuitionistic predicate calculus, developed at the
University of Edinburgh during 1983-1986, by the author together with John
Cartmell and Tatsuya Hagino. The IPE uses an attribute grammar to maintain
the state of its proof tree as a context-sensitive structure. The interface
allows free movement through the proof structure, and encourages a "proof-byexperimentation"
approach, since no proof step is irrevocable.
We describe how the IPE's proof rules can be derived from natural deduction
rules for first-order intuitionistic logic, how these proof rules are encoded as an
attribute grammar, and how the interface is constructed on top of the grammar.
Further facilities for the manipulation of the IPE's proof structures are presented,
including a notion of IPE-tactic for their automatic construction.
We also describe an extension of the IPE to enable the construction and
use of simply-structured collections of axioms and results, the main provision
here being an interactive "theory browser" which looks for facts which match a
selected problem.