Where academic tradition
meets the exciting future

MathEdit: Tool Support for Structured Calculational Proofs

Ralph-Johan Back, Victor Bos, Johannes Eriksson, MathEdit: Tool Support for Structured Calculational Proofs. TUCS Technical Reports 854, Turku Centre for Computer Science, 2007.

Abstract:

The structured calculational proof format emphasizes structure and readability by presenting derivations as outlined sequences of term transformations. The Mathematical Derivation Editor (MathEdit) is an effort to develop tool support for this format. It is a text editor with built-in support for an extensible mathematical syntax and structured derivation notations. In this paper we overview and discuss the features of MathEdit and their implementation: how the editor parses and understands mathematical expressions, determines applicable rules, and how structured derivations are represented. We demonstrate use of MathEdit through example derivations from process algebra.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tBaBoEr07a,
  title = {MathEdit: Tool Support for Structured Calculational Proofs},
  author = {Back, Ralph-Johan and Bos, Victor and Eriksson, Johannes},
  number = {854},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2007},
  ISBN = {978-952-12-2006-7},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication