16 citations · 20 across the 8 of their papers we have counts for
6 papers · 1 filter
The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions
Akihisa Yamada, Benjamin Lucien Kaminski, Dieter Hofbauer +2
This report contains the proceedings of the 19th International Workshop on Termination (WST 2023), which was held in Obergurgl during August 24--25 as part of Obergurgl Summer on R…
Fixed Points Theorems for Non-Transitive Relations
Jérémy Dubut, Akihisa Yamada
In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results a…
Relational Differential Dynamic Logic
Juraj Kolčák, Ichiro Hasuo, Jérémy Dubut +3
In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely re…
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…