EQUATIONAL REASONING SUPPORT FOR ORWELL

Abstract

This report describes the development of an interactive equational reasoning assistant ERA, for an Orwell type notation (Orwell is a functional programming language which is very similar to Miranda; Miranda is a trademark of Research Software Ltd). It is designed to support both proof and program synthesis, using either the inductive or purely calculational styles. Aspects of the tool include pretty printed output, proof schemas, induction hypothesis generation, multiple current proofs, rewriting modulo associativity, and the ability to save proofs mid-stream.