On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
From MaRDI portal
Publication:2405242
DOI10.1007/978-3-319-63046-5_6zbMath1496.03046arXiv1705.08792OpenAlexW2617497701MaRDI QIDQ2405242
Christoph Weidenbach, Marco Voigt, Matthias Horbach
Publication date: 22 September 2017
Full work available at URL: https://arxiv.org/abs/1705.08792
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Combined logics (03B62)
Related Items (2)
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
This page was built for publication: On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
