10 citations · 27 across the 5 of their papers we have counts for
5 papers
Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently
Bertram Felgenhauer
It is known that the first-order theory of rewriting is decidable for ground term rewrite systems, but the general technique uses tree automata and often takes exponential time. Fo…
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.…
A Haskell Library for Term Rewriting
Bertram Felgenhauer, Martin Avanzini, Christian Sternagel
We present a Haskell library for first-order term rewriting covering basic operations on positions, terms, contexts, substitutions and rewrite rules. This effort is motivated by th…