10 citations · 27 across the 5 of their papers we have counts for
3 papers · 1 filter
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.…