39 citations · 219 across the 22 of their papers we have counts for
3 papers · 1 filter
Subtropical Satisfiability
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm +1
Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding const…
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
Thomas Sturm, Marco Voigt, Christoph Weidenbach
We introduce a new decidable fragment of first-order logic with equality, which strictly generalizes two already well-known ones -- the Bernays-Schönfinkel-Ramsey (BSR) Fragment an…
Linear Integer Arithmetic Revisited
Martin Bromberger, Thomas Sturm, Christoph Weidenbach
We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs…