4 citations · 12 across the 11 of their papers we have counts for
11 papers
Left-Linear Completion with AC Axioms
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in…
Generalizing Weighted Path Orders
Teppei Saito, Nao Hirokawa
We show that weighted path orders are special instances of a variant of semantic path orders. Exploiting this fact, we introduce a generalization of weighted path orders that goes…
Hydra Battles and AC Termination
Nao Hirokawa, Aart Middeldorp
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Her…
Compositional Confluence Criteria
Kiraku Shintani, Nao Hirokawa
We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of ort…
Confluence by Critical Pair Analysis Revisited (Extended Version)
Nao Hirokawa, Julian Nagele, Vincent van Oostrom +1
We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule label…
Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel +1
Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstra…