17 citations · 51 across the 10 of their papers we have counts for
10 papers
Certifying Confluence Proofs via Relative Termination and Rule Labeling
Julian Nagele, Bertram Felgenhauer, Harald Zankl
The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based o…
Labelings for Decreasing Diagrams
Harald Zankl, Bertram Felgenhauer, Aart Middeldorp
This article is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We study abstract criteria that allo…
Layer Systems for Proving Confluence
Bertram Felgenhauer, Aart Middeldorp, Harald Zankl +1
We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers.…
Modular Complexity Analysis for Term Rewriting
Harald Zankl, Martin Korp
All current investigations to analyze the derivational complexity of term rewrite systems are based on a single termination method, possibly preceded by transformations. However, t…
Confluence by Decreasing Diagrams -- Formalized
Harald Zankl
This paper presents a formalization of decreasing diagrams in the theorem prover Isabelle. It discusses mechanical proofs showing that any locally decreasing abstract rewrite syste…
Recording Completion for Finding and Certifying Proofs in Equational Logic
Thomas Sternagel, René Thiemann, Harald Zankl +1
When we want to answer/certify whether a given equation is entailed by an equational system we face the following problems: (1) It is hard to find a conversion (but easy to certify…