Konstantin Korovin

Available identifiers

zbMath Open korovin.konstantinMaRDI QIDQ1401931

List of research outcomes

Publication	Date of Publication	Type
Invariant neural architecture for learning term synthesis in instantiation proving	2024-12-09	Paper
Graph sequence learning for premise selection	2024-12-09	Paper
ALASCA: reasoning in quantified linear arithmetic	2023-12-13	Paper
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
Towards conflict-driven learning for virtual substitution	2014-09-08	Paper
Skolemization modulo theories	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
An AC-compatible Knuth-Bendix order.	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

This page was built for person: Konstantin Korovin