Composing Proof Terms
Christina Kohl and Aart Middeldorp
Proceedings of the 27th International Conference on Automated Deduction
(CADE-27), Lecture Notes in Artificial Intelligence 11716,
pp. 337 – 353, 2019.
Abstract
Proof terms are a useful concept for comparing computations in term rewriting. We analyze proof terms with composition, with an eye towards automation. We revisit permutation equivalence and projection equivalence, two key notions presented in the literature. We report on the integration of proof terms with composition into ProTeM, a tool for manipulating proof terms.BibTeX Entry
@inproceedings{KM-CADE19,
author = "Christina Kohl and Aart Middeldorp",
title = "Composing Proof Terms",
booktitle = "Proceedings of the 27th International Conference on Automated
Deduction",
editor = "Pascal Fontaine",
series = "Lecture Notes in Artificial Intelligence",
volume = 11716,
pages = "337--353",
year = 2019,
doi = "10.1007/978-3-030-29436-6\_20"
}