activity
20202024
most citedDeciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings

34 citations · 40 across the 3 of their papers we have counts for

collaborators
Showing cs.LOShow all

2 papers · 1 filter

cs.LO2021

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…

cs.LO2021

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…