## The Design and Implementation of an Interactive Proof
Editor

**Brian Ritchie**
*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-by-experimentation'' 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 fo 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.

**Ph.D thesis - price £7.00**

*LFCS report ECS-LFCS-88-68 (also published as
CST-57-88)*

Previous |

Index |

Next