The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable
From MaRDI portal
Publication:1687561
DOI10.1007/978-3-319-66167-4_14zbMath1496.03032arXiv1706.08504OpenAlexW2652260735MaRDI QIDQ1687561
Publication date: 4 January 2018
Full work available at URL: https://arxiv.org/abs/1706.08504
combination of theorieslinear arithmetic constraintsBernays-Schönfinkel-Ramsey fragmentdifference constraints
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30) Ramsey theory (05D10) Combined logics (03B62)
Related Items (2)
Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
This page was built for publication: The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable