6 citations · 12 across the 8 of their papers we have counts for
5 papers · 1 filter
Graph Sequence Learning for Premise Selection
Edvard K. Holden, Konstantin Korovin
Premise selection is crucial for large theory reasoning as the sheer size of the problems quickly leads to resource starvation. This paper proposes a premise selection approach ins…
AC Simplifications and Closure Redundancies in the Superposition Calculus
André Duarte, Konstantin Korovin
Reasoning in the presence of associativity and commutativity (AC) is well known to be challenging due to prolific nature of these axioms. Specialised treatment of AC axioms is main…
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…
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…
Knuth-Bendix constraint solving is NP-complete
Konstantin Korovin, Andrei Voronkov
We show the NP-completeness of the existential theory of term algebras with the Knuth-Bendix order by giving a nondeterministic polynomial-time algorithm for solving Knuth-Bendix o…