cl-banner

ProTeM: A Proof Term Manipulator (System Description)

Christina Kohl and Aart Middeldorp

2roceedings 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.

 

  PDF |    doi:10.4230/LIPIcs.FSCD.2018.31  

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"
}
Nach oben scrollen