### Certification Redux

Term rewriting is a simple yet powerful model of computation that underlies much of declarative programming and computer assisted theorem proving. Moreover, there are methods to reduce verification tasks of computer programs to ensuring properties of corresponding term rewrite systems. Confluence and termination are arguably the most important properties of term rewriting. While termination states that all computation paths yield a result (thereby making sure that we do not have to wait indefinitely to obtain a result), confluence guarantees that computations are deterministic in the sense that any two computation paths can be joined eventually. Together, termination and confluence imply that independent of the strategy used to compute results, we will always obtain the same result for the same input. Thus, terminating and confluent systems of rewrite rules are of special interest, since they yield decision procedures for their respective equational theories (i.e., equality of two terms modulo a set of equations can be decided by rewriting them both exhaustively and comparing the results). Completion provides a way of transforming a given set of equations into an equivalent set of rewrite rules that is terminating and confluent. In the recent past, certification is very successful in the area of automated termination and confluence proving as well as completion. Where by certification we mean the automatic and reliable verification of proofs that were generated by some untrusted tool (e.g., an automatic termination, confluence, or completion tool). In certification the predominant approach is separated into two stages: First formalize the underlying theory and techniques that are used by untrusted tools with the help of a proof assistant (e.g., Isabelle/HOL). Then, given a proof that was generated by such an untrusted tool, check whether all employed techniques where applied correctly. In the first stage we make sure that the mathematical basis of all used techniques is sound in general and that no implicit assumptions are missing; whereas in the second one their correct application on specific problems is verified rigorously. One of the available certifiers is our tool CeTA, which is code generated from our Isabelle Formalization of Rewriting (IsaFoR), an Isabelle/HOL library that contains many results on rewriting. As our main project goals we strive to extend IsaFoR and CeTA as follows: (1) Add a formalization of the recently introduced weighted path order (WPO). Furthermore, adapt WPO to rewriting modulo associativity and commutativity (AC-rewriting). (2) Support certification of conditional confluence proofs by CeTA. (3) Formalize the theory of AC-rewriting, AC-unification, and normalized completion in order to support certification of normalized completion proofs by CeTA. This will bring CeTA up to speed with the most recent tool developments of termination tools, confluence tools, and completion tools.

project start: February 2015

original project end: January 2018

extended until January 2019

#### Members

- Florian Meßner
- Julian Parsert
- Jonas Schöpf
- Christian Sternagel (coordination)
- Thomas Sternagel
- Akihisa Yamada

#### FWF project number

P27502#### Contact

christian.sternagel@uibk.ac.at#### Publications

Reliable Confluence Analysis of Conditional Term Rewrite Systems

Thomas Sternagel

PhD thesis, University of Innsbruck, 2017.

Certified Non-Confluence with ConCon 1.5

Thomas Sternagel, Christian Sternagel

Proceedings of the 6th International Workshop on Confluence,
2017.

Formalized Ground Completion

Aart Middeldorp, Christian Sternagel

Proceedings of the 6th International Workshop on Confluence,
pp. 51 – 55,
2017.

Infinite Runs in Abstract Completion

Nao Hirokawa, Aart Middeldorp, Sarah Winkler, Christian Sternagel

2nd International Conference on Formal Structures for Computation and Deduction,
Leibniz International Proceedings in Informatics 84,
pp. 19:1-19:16,
2017.

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel

Proceedings of the 14th International Symposium on Frontiers of Combining Systems,
LNCS 10483,
pp. 3-21,
2017.

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems

Christian Sternagel, Thomas Sternagel

Proceedings of the 26th International Confluence on Automated Deduction,
LNCS 10395,
pp. 413-431,
2017.

Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs

Thomas Sternagel and Christian Sternagel

Proceedings of the 5th International Workshop on Confluence (IWC 2016),
pp. 60 – 64,
2016.

A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle

Julian Nagele, Vincent van Oostrom, and Christian Sternagel

Proceedings of the 5th International Workshop on Confluence (IWC 2016),
pp. 55 – 59,
2016.

CoCo 2016 Participant: ConCon

Thomas Sternagel and Aart Middeldorp

Proceedings of the 5th International Workshop on Confluence (IWC 2016),
pp. 81,
2016.

CoCo 2016 Participant: CeTA 2.28

Julian Nagele, Christian Sternagel, and Thomas Sternagel

Proceedings of the 5th International Workshop on Confluence (IWC 2016),
pp. 78,
2016.

The Generalized Subterm Criterion in TTT2

Christian Sternagel

Proceedings of the 15th International Workshop on Termination (WST 2016),
pp. 11:1 – 11:5,
2016.

A Characterization of Quasi-Decreasingness

Thomas Sternagel and Christian Sternagel

Proceedings of the 15th International Workshop on Termination (WST 2016),
pp. 12:1 – 12:5,
2016.

AC Dependency Pairs Revisited

Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016),
Leibniz International Proceedings in Informatics 62,
pp. 8:1 – 8:16,
2016.

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion

Christian Sternagel and Thomas Sternagel

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 29:1-29:16,
2016.

Deriving Comparators and Show Functions in Isabelle/HOL

Christian Sternagel and René Thiemann

Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015),
Lecture Notes in Computer Science 9236,
pp. 421 – 437,
2015.

CoCo Participant: CeTA 2.21

Julian Nagele, Christian Sternagel, Thomas Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl

Proceedings of the 4th International Workshop on Confluence (IWC 2015),
pp. 41,
2015.

Level-Confluence of 3-CTRSs in Isabelle/HOL

Christian Sternagel and Thomas Sternagel

Proceedings of the 4th International Workshop on Confluence (IWC 2015),
pp. 28 – 32,
2015.

Certification of Complexity Proofs using CeTA

Martin Avanzini, Christian Sternagel, and René Thiemann

Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015),
Leibniz International Proceedings in Informatics 36,
pp. 23 – 39,
2015.

Deriving class instances for datatypes

Christian Sternagel and René Thiemann

The Archive of Formal Proofs, 2015.