3 papers
cs.LO2026
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…
cs.LO2025
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…
cs.LO2025
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…