1 citations · 1 across the 4 of their papers we have counts for
4 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),…
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems
Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai +1
Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful meth…
Argument filterings and usable rules in higher-order rewrite systems
Sho Suzuki, Keiichirou Kusakari, Frédéric Blanqui
The static dependency pair method is a method for proving the termination of higher-order rewrite systems a la Nipkow. It combines the dependency pair method introduced for first-o…