5 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…
Automated Analysis of Logically Constrained Rewrite Systems using crest
Jonas Schöpf, Aart Middeldorp
We present crest, a tool for automatically proving (non-)confluence and termination of logically constrained rewrite systems. We compare crest to other tools for logically constrai…
Confluence Criteria for Logically Constrained Rewrite Systems (Full Version)
Jonas Schöpf, Aart Middeldorp
Numerous confluence criteria for plain term rewrite systems are known. For logically constrained rewrite system, an attractive extension of term rewriting in which rules are equipp…