39 citations · 219 across the 22 of their papers we have counts for
5 papers · 1 filter
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…
A Generalized Framework for Virtual Substitution
Marek Kosta, Thomas Sturm
We generalize the framework of virtual substitution for real quantifier elimination to arbitrary but bounded degrees. We make explicit the representation of test points in eliminat…
Better Answers to Real Questions
Marek Kosta, Thomas Sturm, Andreas Dolzmann
We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which a…
Subtropical Real Root Finding
Thomas Sturm
We describe a new incomplete but terminating method for real root finding for large multivariate polynomials. We take an abstract view of the polynomial as the set of exponent vect…