3 papers
cs.LO2021
The ksmt calculus is a -complete decision procedure for non-linear constraints
Franz Brauße, Konstantin Korovin, Margarita V. Korovina +1
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 th…
math.LO2020
On the computability of ordered fields
M. V. Korovina, O. V. Kudinov
In this paper we develop general techniques for classes of computable real numbers generated by subsets of total computable (recursive functions) with special restrictions on basic…
cs.LO2019
A CDCL-style calculus for solving non-linear constraints
Franz Brauße, Konstantin Korovin, Margarita Korovina +1
In this paper we propose a novel approach for checking satisfiability of non-linear constraints over the reals, called ksmt. The procedure is based on conflict resolution in CDCL s…