Composing Proof Terms

Christina Kohl and Aart Middeldorp

27th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 11716, pp. 337 – 353, 2019.


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.


  PDF |    doi:10.1007/978-3-030-29436-6_20  |  © Open Access (CC BY 4.0)


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