×

Korovin, Konstantin

Author ID: korovin.konstantin Recent zbMATH articles by "Korovin, Konstantin"
Published as: Korovin, Konstantin
Documents Indexed: 31 Publications since 2001
Co-Authors: 15 Co-Authors with 28 Joint Publications
237 Co-Co-Authors

Publications by Year

Citations contained in zbMATH Open

24 Publications have been cited 183 times in 116 Documents Cited by Year
iProver – an instantiation-based theorem prover for first-order logic. (System description). Zbl 1165.68462
Korovin, Konstantin
46
2008
Inst-Gen – a modular approach to instantiation-based automated reasoning. Zbl 1385.68038
Korovin, Konstantin
19
2013
Integrating linear arithmetic into superposition calculus. Zbl 1179.03018
Korovin, Konstantin; Voronkov, Andrei
16
2007
Conflict resolution. Zbl 1336.68236
Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei
10
2009
Theory instantiation. Zbl 1165.03315
Ganzinger, Harald; Korovin, Konstantin
10
2006
Integrating equational reasoning into instantiation-based theorem proving. Zbl 1095.68111
Ganzinger, Harald; Korovin, Konstantin
10
2004
Implementing superposition in iProver (system description). Zbl 07614685
Duarte, André; Korovin, Konstantin
10
2020
Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079
Korovin, Konstantin; Voronkov, Andrei
9
2003
iProver-Eq: an instantiation-based theorem prover with equality. Zbl 1291.68354
Korovin, Konstantin; Sticksel, Christoph
8
2010
Non-cyclic sorts for first-order satisfiability. Zbl 1398.68484
Korovin, Konstantin
6
2013
Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. Zbl 1485.68282
Holden, Edvard K.; Korovin, Konstantin
5
2021
An abstraction-refinement framework for reasoning with large theories. Zbl 1511.68326
Lopez Hernandez, Julio Cesar; Korovin, Konstantin
4
2018
AC simplifications and closure redundancies in the superposition calculus. Zbl 07532517
Duarte, André; Korovin, Konstantin
4
2021
A CDCL-style calculus for solving non-linear constraints. Zbl 1435.68300
Brauße, Franz; Korovin, Konstantin; Korovina, Margarita; Müller, Norbert
4
2019
Solving systems of linear inequalities by bound propagation. Zbl 1341.68193
Korovin, Konstantin; Voronkov, Andrei
3
2011
Predicate elimination for preprocessing in first-order theorem proving. Zbl 1475.68441
Khasidashvili, Zurab; Korovin, Konstantin
3
2016
Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045
Korovin, Konstantin; Voronkov, Andrei
3
2001
An AC-compatible Knuth-Bendix order. Zbl 1278.68268
Korovin, Konstantin; Voronkov, Andrei
2
2003
Labelled unit superposition calculi for instantiation-based reasoning. Zbl 1306.68192
Korovin, Konstantin; Sticksel, Christoph
2
2010
EPR-based bounded model checking at word level. Zbl 1358.68190
Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei
2
2012
Towards conflict-driven learning for virtual substitution. Zbl 1416.68166
Korovin, Konstantin; Koša, Marek; Sturm, Thomas
2
2014
Ground joinability and connectedness in the superposition calculus. Zbl 07628187
Duarte, André; Korovin, Konstantin
2
2022
The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints. Zbl 07437075
Brauße, Franz; Korovin, Konstantin; Korovina, Margarita V.; Müller, Norbert Th.
2
2021
Verifying orientability of rewrite rules using the Knuth-Bendix order. Zbl 0981.68072
Korovin, Konstantin; Voronkov, Andrei
1
2001
Ground joinability and connectedness in the superposition calculus. Zbl 07628187
Duarte, André; Korovin, Konstantin
2
2022
Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. Zbl 1485.68282
Holden, Edvard K.; Korovin, Konstantin
5
2021
AC simplifications and closure redundancies in the superposition calculus. Zbl 07532517
Duarte, André; Korovin, Konstantin
4
2021
The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints. Zbl 07437075
Brauße, Franz; Korovin, Konstantin; Korovina, Margarita V.; Müller, Norbert Th.
2
2021
Implementing superposition in iProver (system description). Zbl 07614685
Duarte, André; Korovin, Konstantin
10
2020
A CDCL-style calculus for solving non-linear constraints. Zbl 1435.68300
Brauße, Franz; Korovin, Konstantin; Korovina, Margarita; Müller, Norbert
4
2019
An abstraction-refinement framework for reasoning with large theories. Zbl 1511.68326
Lopez Hernandez, Julio Cesar; Korovin, Konstantin
4
2018
Predicate elimination for preprocessing in first-order theorem proving. Zbl 1475.68441
Khasidashvili, Zurab; Korovin, Konstantin
3
2016
Towards conflict-driven learning for virtual substitution. Zbl 1416.68166
Korovin, Konstantin; Koša, Marek; Sturm, Thomas
2
2014
Inst-Gen – a modular approach to instantiation-based automated reasoning. Zbl 1385.68038
Korovin, Konstantin
19
2013
Non-cyclic sorts for first-order satisfiability. Zbl 1398.68484
Korovin, Konstantin
6
2013
EPR-based bounded model checking at word level. Zbl 1358.68190
Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei
2
2012
Solving systems of linear inequalities by bound propagation. Zbl 1341.68193
Korovin, Konstantin; Voronkov, Andrei
3
2011
iProver-Eq: an instantiation-based theorem prover with equality. Zbl 1291.68354
Korovin, Konstantin; Sticksel, Christoph
8
2010
Labelled unit superposition calculi for instantiation-based reasoning. Zbl 1306.68192
Korovin, Konstantin; Sticksel, Christoph
2
2010
Conflict resolution. Zbl 1336.68236
Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei
10
2009
iProver – an instantiation-based theorem prover for first-order logic. (System description). Zbl 1165.68462
Korovin, Konstantin
46
2008
Integrating linear arithmetic into superposition calculus. Zbl 1179.03018
Korovin, Konstantin; Voronkov, Andrei
16
2007
Theory instantiation. Zbl 1165.03315
Ganzinger, Harald; Korovin, Konstantin
10
2006
Integrating equational reasoning into instantiation-based theorem proving. Zbl 1095.68111
Ganzinger, Harald; Korovin, Konstantin
10
2004
Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079
Korovin, Konstantin; Voronkov, Andrei
9
2003
An AC-compatible Knuth-Bendix order. Zbl 1278.68268
Korovin, Konstantin; Voronkov, Andrei
2
2003
Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045
Korovin, Konstantin; Voronkov, Andrei
3
2001
Verifying orientability of rewrite rules using the Knuth-Bendix order. Zbl 0981.68072
Korovin, Konstantin; Voronkov, Andrei
1
2001
all top 5

Cited by 175 Authors

14 Weidenbach, Christoph
11 Korovin, Konstantin
9 Voronkov, Andrei
8 Bonacina, Maria Paola
5 Reger, Giles
5 Tinelli, Cesare
4 Baumgartner, Peter
4 Blanchette, Jasmin Christian
4 de Moura, Leonardo
4 Kovács, Laura Ildikó
4 Middeldorp, Aart
4 Plaisted, David Alan
4 Reynolds, Andrew
4 Sutcliffe, Geoff
4 Winkler, Sarah
3 Brown, Chad Edward
3 Duarte, André
3 Hirokawa, Nao
3 Schulz, Stephan
3 Urban, Josef
3 Vukmirović, Petar
2 Barrett, Clark W.
2 Biere, Armin
2 Bjørner, Nikolaj S.
2 Brauße, Franz
2 Bromberger, Martin
2 Burel, Guillaume
2 Cheney, James
2 Cimatti, Alessandro
2 Cruanes, Simon
2 Desharnais, Martin
2 Gauthier, Thibault
2 Griggio, Alberto
2 Heule, Marijn J. H.
2 Jovanović, Dejan
2 Kaliszyk, Cezary
2 Korovina, Margarita Vladimirovna
2 Kruglov, Evgeniĭ Valentinovich
2 Leidinger, Hendrik
2 Lynch, Christopher A.
2 Müller, Norbert Th.
2 Nicolini, Enrica
2 Rawson, Michael
2 Scholl, Christoph
2 Sebastiani, Roberto
2 Síč, Juraj
2 Suda, Martin
2 Teucke, Andreas
2 Tourret, Sophie
2 Tran, Duc-Khanh
2 Waldmann, Uwe
2 Wimmer, Ralf D.
2 Zankl, Harald
1 Alagi, Gábor
1 Althaus, Ernst
1 Asperti, Andrea
1 Becker, Bernd
1 Beeson, Michael J.
1 Benzmüller, Christoph Ewald
1 Bhayat, Ahmed
1 Bigarella, Filippo
1 Bury, Guillaume
1 Cauderlier, Raphaël
1 Conchon, Sylvain
1 Danas, Ryan
1 Delahaye, David
1 Dolzmann, Andreas
1 Dougherty, Daniel J.
1 Dragoste, Irina
1 Dross, Claire
1 Dwyer, Matthew B.
1 Echenim, Mnacho
1 Eisenhofer, Clemens
1 Faqeh, Rasha
1 Feng, Yanghe
1 Fetzer, Christof
1 Fietzke, Arnaud
1 Fiori, Alberto
1 Fröhlich, Andreas M.
1 Fu, Huimin
1 Garvin, Brady J.
1 Ge-Ernst, Aile
1 Georgiou, Pamina
1 Ghilardi, Silvio
1 Giese, Martin A.
1 Giesl, Jürgen
1 Graham-Lengrand, Stéphane
1 Halmagrand, Pierre
1 He, Xingxing
1 Hermant, Olivier
1 Holden, Edvard K.
1 Hůla, Jan
1 Iosif, Radu
1 Irfan, Ahmed
1 Jakubův, Jan
1 Janičić, Predrag
1 Janota, Mikoláš
1 Järvisalo, Matti
1 Ji, Kailiang
1 Jonáš, Martin
...and 75 more Authors

Citations by Year