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.08792MaRDI QIDQ2405242
Christoph Weidenbach, Marco Voigt, Matthias Horbach
Publication date: 22 September 2017
Full work available at URL: https://arxiv.org/abs/1705.08792
03B25: Decidability of theories and sets of sentences
03B35: Mechanization of proofs and logical operations
03B62: Combined logics
Related Items
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates