Automating Proof Terms in Term Rewriting

Automating Proof Terms in Term Rewriting

Aart Middeldorp

University of Innsbruck

2018/09/20 (Thu) 14:00 to 15:00
I-56 (Collaboration Room 7) on 5F of IS Building III at JAIST
Logic Unit

Proof terms are a useful concept for reasoning about computations in term rewriting. This talk gives an introduction to proof terms and mentions some of the challenges when reasoning about proof terms. Since human calculation with proof terms is tedious and error-prone, the tool ProTeM was developed that offers support for manipulating proof terms in left-linear rewrite systems. We use ProTeM throughout the talk to illustrate the various operations on proof terms. The talk is based on joint work with Christina Kohl.

Nao Hirokawa