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.
pdf
doi:10.4230/LIPIcs.FSCD.2018.31
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"}