Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic.

Erika Ábrahám James H. Davenport Matthew England Gereon Kremer

Published in: CoRR (2021)

Keyphrases

quantifier free
quantifier elimination
first order logic
rewrite systems
sat solvers
constraint propagation