Konstantin Korovin

Available identifiers

zbMath Open korovin.konstantinMaRDI QIDQ1401931

List of research outcomes

Publication	Date of Publication	Type
The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints	2023-09-21	Paper
Ground joinability and connectedness in the superposition calculus	2022-12-07	Paper
Implementing Superposition in iProver (System Description)	2022-11-09	Paper
AC simplifications and closure redundancies in the superposition calculus	2022-05-25	Paper
Heterogeneous heuristic optimisation and scheduling for first-order theorem proving	2022-04-22	Paper
The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints	2021-12-01	Paper
A CDCL-style calculus for solving non-linear constraints	2020-05-13	Paper
An abstraction-refinement framework for reasoning with large theories	2018-10-18	Paper
Knuth--bendix constraint solving is NP-complete	2017-07-12	Paper
Predicate Elimination for Preprocessing in First-Order Theorem Proving	2016-09-05	Paper
GoRRiLA and Hard Reality	2015-12-07	Paper
Implementing Conflict Resolution	2015-12-07	Paper
Skolemization Modulo Theories	2014-09-08	Paper
Towards Conflict-Driven Learning for Virtual Substitution	2014-09-08	Paper
Non-cyclic Sorts for First-Order Satisfiability	2013-09-20	Paper
Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning	2013-04-19	Paper
EPR-Based Bounded Model Checking at Word Level	2012-09-05	Paper
Solving Systems of Linear Inequalities by Bound Propagation	2011-07-29	Paper
Labelled Unit Superposition Calculi for Instantiation-Based Reasoning	2010-10-12	Paper
iProver-Eq: An Instantiation-Based Theorem Prover with Equality	2010-09-14	Paper
Automated Deduction – CADE-19	2010-04-20	Paper
Conflict Resolution	2009-10-09	Paper
Integrating Linear Arithmetic into Superposition Calculus	2009-03-05	Paper
iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)	2008-11-27	Paper
Theory Instantiation	2008-05-27	Paper
Mathematical Foundations of Computer Science 2005	2006-10-20	Paper
Computer Science Logic	2005-08-22	Paper
Orienting rewrite rules with the Knuth-Bendix order.	2003-08-19	Paper
https://portal.mardi4nfdi.de/entity/Q4415258	2003-07-28	Paper
https://portal.mardi4nfdi.de/entity/Q4535077	2002-06-12	Paper
https://portal.mardi4nfdi.de/entity/Q2778876	2002-03-21	Paper

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Konstantin Korovin