Composing Proof Terms
Christina Kohl, Aart Middeldorp · Lecture notes in computer science · 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.