Automating Proof Terms in Term Rewriting
- Aart Middeldorp
University of Innsbruck
- homepage
| Date: | 2018/09/20 (Thu) 14:00 to 15:00 |
|---|---|
| Place: | I-56 (Collaboration Room 7) on 5F of IS Building III at JAIST |
| Group: | 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.
| Contact | Nao Hirokawa |
|---|