34 citations · 40 across the 3 of their papers we have counts for
5 papers
Extensions of the Cylindrical Algebraic Covering Method for Quantifiers
Jasper Nalbach, Gereon Kremer
The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cyl…
On the proof complexity of MCSAT
Gereon Kremer, Erika Abraham, Vijay Ganesh
Satisfiability Modulo Theories (SMT) and SAT solvers are critical components in many formal software tools, primarily due to the fact that they are able to easily solve logical pro…
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Erika Abraham, James H. Davenport, Matthew England +1
We discuss the topic of unsatisfiability proofs in SMT, particularly with reference to quantifier free non-linear real arithmetic. We outline how the methods here do not admit triv…
New Opportunities for the Formal Proof of Computational Real Geometry?
Erika {Á}brahám, James Davenport, Matthew England +2
The purpose of this paper is to explore the question "to what extent could we produce formal, machine-verifiable, proofs in real algebraic geometry?" The question has been asked be…
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
Erika Ábrahám, James H. Davenport, Matthew England +1
We present a new algorithm for determining the satisfiability of conjunctions of non-linear polynomial constraints over the reals, which can be used as a theory solver for satisfia…