ProTeM: A Proof Term Manipulator (System Description)
Christina Kohl and Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for
Computation and Deduction (FSCD 2018), Leibniz International Proceedings in
Informatics 108, pp. 31:1 – 31:8, 2018.
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 Entry
@inproceedings{KM-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",
editor = "H\'el\`ene Kirchner",
series = "Leibniz International Proceedings in Informatics"
volume = 108,
pages = "31:1--31:8",
year = 2018,
doi = "10.4230/LIPIcs.FSCD.2018.31"
}