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.
Previous | Index | Next An error occured whilst processing this directive