The ksmt calculus is a $\delta$-complete decision procedure for non-linear constraints
Logic in Computer Science
2021-04-28 v1
Abstract
ksmt is a CDCL-style calculus for solving non-linear constraints over real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the ksmt calculus and show that it is a -complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.
Keywords
Cite
@article{arxiv.2104.13269,
title = {The ksmt calculus is a $\delta$-complete decision procedure for non-linear constraints},
author = {Franz Brauße and Konstantin Korovin and Margarita V. Korovina and Norbert Th. Müller},
journal= {arXiv preprint arXiv:2104.13269},
year = {2021}
}
Comments
The conference version of this paper is accepted at CADE-28