Ritchie, Brian

2013-04-02T15:18:04Z

2013-04-02T15:18:04Z

1988

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 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.

http://hdl.handle.net/1842/6607

en

The University of Edinburgh

Ritchie, B., Interactive Proof Construction, in IEE Colloquium on "Theorem Provers in Theory and in Practice, Institution of Electrical Engineers Digest No. 1987/39, 1987.

interactive proof editor

IPE

context-sensitive structure.

attribute grammar

Design and implementation of an interactive proof editor

The design and implementation of an interactive proof editor

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy