Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
Abstract elided by the publisher.
Related papers
- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic TACAS 2022
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI 2017
- Quantified class constraints Haskell 2017
- Solving String Constraints Using SAT CAV 2023
- sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses CAV 2025
- String solving with word equations and transducers: towards a logic for analysing mutation XSS POPL 2016
- From Clauses to Klauses CAV 2024
- Languages with Decidable Learning: A Meta-theorem OOPSLA 2023