The Interactive Proof Editor: An Experiment in Interactive Theorem

B. Ritchie and P. Taylor

Abstract: The IPE is an interactive editor for proof in intuitionistic first order logic, extended with formula schemas to allow the expression of induction principles. In this paper we describe the IPE - giving example proofs and an overview of the proof facilities it provides. In addition we discuss some of the advantages, which flow from interactive proof, and describe further facilities for proof editing suggested by the use of IPE.

LFCS report ECS-LFCS-88-61

Previous | Index | Next