ProTeM: A Proof Term Manipulator (System Description)

Authors Christina Kohl , Aart Middeldorp

Thumbnail PDF


  • Filesize: 0.54 MB
  • 8 pages

Document Identifiers

Author Details

Christina Kohl
  • Department of Computer Science, University of Innsbruck, Austria
Aart Middeldorp
  • Department of Computer Science, University of Innsbruck, Austria

Cite AsGet BibTex

Christina Kohl and Aart Middeldorp. ProTeM: A Proof Term Manipulator (System Description). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 31:1-31:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Equational logic and rewriting
  • Proof terms
  • term rewriting
  • interactive tool


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. H.J. Sander Bruggink. Equivalence of Reductions in Higher-Order Rewriting. PhD thesis, Utrecht University, 2008. Google Scholar
  2. Nao Hirokawa and Aart Middeldorp. Decreasing diagrams and relative termination. Journal of Automated Reasoning, 47(4):481-501, 2011. URL:
  3. Nao Hirokawa and Aart Middeldorp. Commutation via relative termination. In Proc. 2nd International Workshop on Confluence, pages 29-33, 2013. Google Scholar
  4. Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797-821, 1980. URL:
  5. Carlos Lombardi, Alejandro Ríos, and Roel de Vrijer. Proof terms for infinitary rewriting. In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of Lecture Notes in Computer Science (Advanced Research in Computing and Software Science), pages 303-318, 2014. URL:
  6. Claude Marché, Albert Rubio, and Hans Zantema. Termination problem data base: Format of input files. Accessed: 2018-17-01.
  7. Julian Nagele. Mechanizing Confluence. PhD thesis, University of Innsbruck, 2017. Google Scholar
  8. Julian Nagele and Aart Middeldorp. Certification of classical confluence results for left-linear term rewrite systems. In Proc. 7th International Conference on Interactive Theorem Proving, volume 9807 of Lecture Notes in Computer Science, pages 290-306, 2016. URL:
  9. Terese, editor. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  10. Vaadin framework 8. Accessed: 2018-17-01.
  11. Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. URL:
  12. Vincent van Oostrom and Roel de Vrijer. Four equivalent equivalences of reductions. In Proc. 2nd International Workshop on Reduction Strategies in Rewriting and Programming, volume 70(6) of Electronic Notes in Theoretical Computer Science, pages 21-61, 2002. URL: