research
∙
07/26/2023
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
As for term rewrite systems, the dependency pair (DP, for short) framewo...
share
research
∙
02/22/2019
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
The grammar representation of a narrowing tree for a syntactically deter...
research
∙
02/22/2019
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
In this paper, we show a new approach to transformations of an imperativ...
research
∙
06/19/2018
A Theory of Reversibility for Erlang
In a reversible language, any forward computation can be undone by a fin...
research
∙
02/19/2018
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers
In the dependency pair framework for proving termination of rewriting sy...
research
∙
02/19/2018
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
A proof tableau of Hoare logic is an annotated program with pre- and pos...
research
∙
10/08/2017