The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable

DOI10.1007/978-3-319-66167-4_14zbMath1496.03032arXiv1706.08504OpenAlexW2652260735MaRDI QIDQ1687561

Marco Voigt

Publication date: 4 January 2018

Full work available at URL: https://arxiv.org/abs/1706.08504

zbMATH Keywords

combination of theorieslinear arithmetic constraintsBernays-Schönfinkel-Ramsey fragmentdifference constraints

Mathematics Subject Classification ID

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