Author:Konstantin Korovin

Publications
Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification (Extended Version) Johannes Schoisswohl, Laura Kovács, Konstantin Korovin and Andrei Voronkov EasyChair Preprint 16032
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version) Johannes Schoisswohl, Laura Kovács and Konstantin Korovin EasyChair Preprint 13150
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification Johannes Schoisswohl, Laura Kovács, Konstantin Korovin and Andrei Voronkov In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic Johannes Schoisswohl, Laura Kovács and Konstantin Korovin In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Guiding an Instantiation Prover with Graph Neural Networks Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock and Josef Urban In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Refining Unification with Abstraction Ahmed Bhayat, Konstantin Korovin, Laura Kovacs and Johannes Schoisswohl In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Towards an Abstraction-Refinement Framework for Reasoning with Large Theories Julio Cesar Lopez Hernandez and Konstantin Korovin In:IWIL Workshop and LPAR Short Presentations
EPR-based k-induction with Counterexample Guided Abstraction Refinement Zurab Khasidashvili, Konstantin Korovin and Dmitry Tsarkov In:GCAI 2015. Global Conference on Artificial Intelligence
Instantiations, Zippers and EPR Interpolation Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav In:LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers) Stephan Schulz, Konstantin Korovin and Michael Rawson (editors) Kalpa Publications in Computing, volume 23
Proceedings of the 14th and 15th International Workshops on the Implementation of Logics Konstantin Korovin, Stephan Schulz and Michael Rawson (editors) Kalpa Publications in Computing, volume 21
ANDREI-60. Automated New-era Deductive Reasoning Event in Iberia Laura Kovacs, Konstantin Korovin and Giles Reger (editors) EPiC Series in Computing, volume 68
LPAR-22 Workshop and Short Paper Proceedings Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe and Margus Veanes (editors) Kalpa Publications in Computing, volume 9
UNIF 2012 Post-Worskhop Proceedings. The 26th International Workshop on Unification Santiago Escobar, Konstantin Korovin and Vladimir Rybakov (editors) EPiC Series in Computing, volume 24
IWIL 2012. The 9th International Workshop on the Implementation of Logics Konstantin Korovin, Stephan Schulz and Eugenia Ternovska (editors) EPiC Series in Computing, volume 22
UNIF 2013. 27th International Workshop on Unification Konstantin Korovin and Barbara Morawska (editors) EPiC Series in Computing, volume 19

Keyphrases

abstraction refinement, arithmetic², automated reasoning⁴, automated theorem proving, Bounded Model Checking, Clause Evaluation, decision procedure, Descision Procedure, EPR, EPR fragment, first-order logic, first-order theorem proving², Graph Neural Networks, interpolation, k-induction, LIA, linear arithmetic⁴, LIRA², literal selection², logic, LRA, machine learning, Presburger arithmetic, Quantified First-Order Logic, quantifier elimination², real arithmetic², redundancy², simplification, SMT⁶, superposition², theorem proving³, unification, Unification with Abstraction, virtual substitution.