16 citations · 20 across the 8 of their papers we have counts for
3 papers · 1 filter
Nagoya Termination Tool
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first i…
A Unified Ordering for Termination Proving
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
We introduce a reduction order called the weighted path order (WPO) that subsumes many existing reduction orders. WPO compares weights of terms as in the Knuth-Bendix order (KBO),…
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…