35 citations · 65 across the 12 of their papers we have counts for
12 papers
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
Ayuka Matsumi, Naoki Nishida, Misaki Kojima +1
As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewri…
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
Naoki Nishida, Yuya Maeda
The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expr…
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Yoshiaki Kanazawa, Naoki Nishida
In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The r…
A Theory of Reversibility for Erlang
Ivan Lanese, Naoki Nishida, Adrián Palacios +1
In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programmin…
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai +1
In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences…
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
Shinnosuke Mizutani, Naoki Nishida
A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tab…