4 citations · 12 across the 11 of their papers we have counts for
11 papers · 1 filter
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…
Critical Peaks Redefined -
Nao Hirokawa, Julian Nagele, Vincent van Oostrom +1
Let a cluster be a term with a number of patterns occurring in it. We give two accounts of clusters, a geometric one as sets of (node and edge) positions, and an inductive one as p…
AC-KBO Revisited
Akihisa Yamada, Sarah Winkler, Nao Hirokawa +1
Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-f…
Uncurrying for Innermost Termination and Derivational Complexity
Harald Zankl, Nao Hirokawa, Aart Middeldorp
First-order applicative term rewriting systems provide a natural framework for modeling higher-order aspects. In earlier work we introduced an uncurrying transformation which is te…
Automated Complexity Analysis Based on the Dependency Pair Method
Nao Hirokawa, Georg Moser
This article is concerned with automated complexity analysis of term rewrite systems. Since these systems underlie much of declarative programming, time complexity of functions def…
Decreasing Diagrams and Relative Termination
Nao Hirokawa, Aart Middeldorp
In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system R is confluent if all its critical pairs are joinable and the critical pair st…