Abstract

Proof terms are a useful concept for reasoning about computations in term rewriting. Human calculation with proof terms is tedious and error-prone. We present ProTeM, a new tool that offers support for manipulating proof terms that represent multisteps in left-linear rewrite systems.

BibTeX

@inproceedings{CKAM-FSCD18,
  author    = "Christina Kohl and Aart Middeldorp",
  title     = "{ProTeM}: A Proof Term Manipulator (System Description)",
  booktitle = "Proceedings of the 3rd International Conference on Formal
               Structures for Computation and Deduction (FSCD 2018)",
  editor    = "H{\'e}l{\`e}ne Kirchner",
  series    = "Leibniz International Proceedings in Informatics"
  volume    = 108,
  pages     = "31:1--31:8",
  year      = 2018,
  doi       = "10.4230/LIPIcs.FSCD.2018.31"
}