13 citations · 19 across the 6 of their papers we have counts for
6 papers
Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version)
Takahito Aoto, Naoki Nishida, Jonas Schöpf
Logically constrained term rewrite systems (LCTRSs) are a rewriting formalism that naturally supports built-in data structures, including integers and bit-vectors. The recent frame…
Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)
Kanta Takahata, Jonas Schöpf, Naoki Nishida +1
Logically constrained term rewriting is a relatively new rewriting formalism that naturally supports built-in data structures, such as integers and bit vectors. In the analysis of…
Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version)
Kanta Takahata, Jonas Schöpf, Naoki Nishida +1
Logically constrained term rewriting is a rewriting framework that supports built-in data structures such as integers and bit vectors. Recently, constrained terms play a key role i…
Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)
Takahito Aoto, Naoki Nishida, Jonas Schöpf
Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances wit…
Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems
Takahito Aoto, Yoshihito Toyama
The notion of normal forms is ubiquitous in various equivalent transformations. Confluence (CR), one of the central properties of term rewriting systems (TRSs), concerns uniqueness…
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
Takahito Aoto, Yoshihito Toyama
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewri…