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

@inproceedings{CKAM-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"
}