ProTeM: A Proof Term Manipulator (System Description)
Christina Kohl, Aart Middeldorp · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 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.