5 citations · 9 across the 4 of their papers we have counts for
5 papers
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…
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…
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…
The Rice-Shapiro theorem in Computable Topology
Margarita Korovina, Oleg Kudinov
We provide requirements on effectively enumerable topological spaces which guarantee that the Rice-Shapiro theorem holds for the computable elements of these spaces. We show that t…
Making big steps in trajectories
Norbert Th. Müller, Margarita Korovina
We consider the solution of initial value problems within the context of hybrid systems and emphasise the use of high precision approximations (in software for exact real arithmeti…