Edit Profile (opens in new tab) Korovin, Konstantin Compute Distance To: Compute Author ID: korovin.konstantin Published as: Korovin, Konstantin Documents Indexed: 30 Publications since 2001 Co-Authors: 15 Co-Authors with 27 Joint Publications 223 Co-Co-Authors all top 5 Co-Authors 3 single-authored 13 Voronkov, Andrei 3 Duarte, André 3 Sticksel, Christoph 2 Brauße, Franz 2 Ganzinger, Harald 2 Khasidashvili, Zurab O. 2 Korovina, Margarita Vladimirovna 2 Müller, Norbert Th. 2 Tsiskaridze, Nestan 1 Emmer, Moshe 1 Holden, Edvard K. 1 Koša, Marek 1 López-Hernández, Julio César 1 Sturm, Thomas 1 Veanes, Margus Serials 1 Information and Computation 1 ACM Transactions on Computational Logic Fields 28 Computer science (68-XX) 10 Mathematical logic and foundations (03-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 1 Operations research, mathematical programming (90-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 21 Publications have been cited 146 times in 101 Documents Cited by ▼ Year ▼ iProver – an instantiation-based theorem prover for first-order logic. (System description). Zbl 1165.68462Korovin, Konstantin 42 2008 Inst-Gen – a modular approach to instantiation-based automated reasoning. Zbl 1385.68038Korovin, Konstantin 16 2013 Integrating linear arithmetic into superposition calculus. Zbl 1179.03018Korovin, Konstantin; Voronkov, Andrei 14 2007 Integrating equational reasoning into instantiation-based theorem proving. Zbl 1095.68111Ganzinger, Harald; Korovin, Konstantin 10 2004 Theory instantiation. Zbl 1165.03315Ganzinger, Harald; Korovin, Konstantin 10 2006 Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079Korovin, Konstantin; Voronkov, Andrei 8 2003 Conflict resolution. Zbl 1336.68236Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei 7 2009 iProver-Eq: an instantiation-based theorem prover with equality. Zbl 1291.68354Korovin, Konstantin; Sticksel, Christoph 7 2010 Non-cyclic sorts for first-order satisfiability. Zbl 1398.68484Korovin, Konstantin 5 2013 Implementing superposition in iProver (system description). Zbl 07614685Duarte, André; Korovin, Konstantin 5 2020 Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045Korovin, Konstantin; Voronkov, Andrei 3 2001 A CDCL-style calculus for solving non-linear constraints. Zbl 1435.68300Brauße, Franz; Korovin, Konstantin; Korovina, Margarita; Müller, Norbert 3 2019 An abstraction-refinement framework for reasoning with large theories. Zbl 06958129Lopez Hernandez, Julio Cesar; Korovin, Konstantin 3 2018 Solving systems of linear inequalities by bound propagation. Zbl 1341.68193Korovin, Konstantin; Voronkov, Andrei 2 2011 Labelled unit superposition calculi for instantiation-based reasoning. Zbl 1306.68192Korovin, Konstantin; Sticksel, Christoph 2 2010 An AC-compatible Knuth-Bendix order. Zbl 1278.68268Korovin, Konstantin; Voronkov, Andrei 2 2003 EPR-based bounded model checking at word level. Zbl 1358.68190Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei 2 2012 Predicate elimination for preprocessing in first-order theorem proving. Zbl 1475.68441Khasidashvili, Zurab; Korovin, Konstantin 2 2016 The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints. Zbl 07437075Brauße, Franz; Korovin, Konstantin; Korovina, Margarita V.; Müller, Norbert Th. 1 2021 Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. Zbl 1485.68282Holden, Edvard K.; Korovin, Konstantin 1 2021 AC simplifications and closure redundancies in the superposition calculus. Zbl 07532517Duarte, André; Korovin, Konstantin 1 2021 The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints. Zbl 07437075Brauße, Franz; Korovin, Konstantin; Korovina, Margarita V.; Müller, Norbert Th. 1 2021 Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. Zbl 1485.68282Holden, Edvard K.; Korovin, Konstantin 1 2021 AC simplifications and closure redundancies in the superposition calculus. Zbl 07532517Duarte, André; Korovin, Konstantin 1 2021 Implementing superposition in iProver (system description). Zbl 07614685Duarte, André; Korovin, Konstantin 5 2020 A CDCL-style calculus for solving non-linear constraints. Zbl 1435.68300Brauße, Franz; Korovin, Konstantin; Korovina, Margarita; Müller, Norbert 3 2019 An abstraction-refinement framework for reasoning with large theories. Zbl 06958129Lopez Hernandez, Julio Cesar; Korovin, Konstantin 3 2018 Predicate elimination for preprocessing in first-order theorem proving. Zbl 1475.68441Khasidashvili, Zurab; Korovin, Konstantin 2 2016 Inst-Gen – a modular approach to instantiation-based automated reasoning. Zbl 1385.68038Korovin, Konstantin 16 2013 Non-cyclic sorts for first-order satisfiability. Zbl 1398.68484Korovin, Konstantin 5 2013 EPR-based bounded model checking at word level. Zbl 1358.68190Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei 2 2012 Solving systems of linear inequalities by bound propagation. Zbl 1341.68193Korovin, Konstantin; Voronkov, Andrei 2 2011 iProver-Eq: an instantiation-based theorem prover with equality. Zbl 1291.68354Korovin, Konstantin; Sticksel, Christoph 7 2010 Labelled unit superposition calculi for instantiation-based reasoning. Zbl 1306.68192Korovin, Konstantin; Sticksel, Christoph 2 2010 Conflict resolution. Zbl 1336.68236Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei 7 2009 iProver – an instantiation-based theorem prover for first-order logic. (System description). Zbl 1165.68462Korovin, Konstantin 42 2008 Integrating linear arithmetic into superposition calculus. Zbl 1179.03018Korovin, Konstantin; Voronkov, Andrei 14 2007 Theory instantiation. Zbl 1165.03315Ganzinger, Harald; Korovin, Konstantin 10 2006 Integrating equational reasoning into instantiation-based theorem proving. Zbl 1095.68111Ganzinger, Harald; Korovin, Konstantin 10 2004 Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079Korovin, Konstantin; Voronkov, Andrei 8 2003 An AC-compatible Knuth-Bendix order. Zbl 1278.68268Korovin, Konstantin; Voronkov, Andrei 2 2003 Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045Korovin, Konstantin; Voronkov, Andrei 3 2001 all cited Publications top 5 cited Publications all top 5 Cited by 158 Authors 13 Weidenbach, Christoph 10 Korovin, Konstantin 9 Voronkov, Andrei 7 Bonacina, Maria Paola 4 Baumgartner, Peter 4 Middeldorp, Aart 4 Plaisted, David Alan 4 Reger, Giles 4 Tinelli, Cesare 3 Blanchette, Jasmin Christian 3 Brown, Chad Edward 3 de Moura, Leonardo 3 Duarte, André 3 Hirokawa, Nao 3 Kovács, Laura Ildikó 3 Reynolds, Andrew 3 Schulz, Stephan 3 Sutcliffe, Geoff 3 Winkler, Sarah 2 Biere, Armin 2 Bromberger, Martin 2 Burel, Guillaume 2 Cheney, James 2 Cruanes, Simon 2 Heule, Marijn J. H. 2 Jovanović, Dejan 2 Kaliszyk, Cezary 2 Kruglov, Evgeniĭ Valentinovich 2 Lynch, Christopher A. 2 Nicolini, Enrica 2 Rawson, Michael 2 Síč, Juraj 2 Suda, Martin 2 Teucke, Andreas 2 Tourret, Sophie 2 Tran, Duc-Khanh 2 Urban, Josef 2 Vukmirović, Petar 2 Waldmann, Uwe 2 Woltzenlogel Paleo, Bruno 2 Zankl, Harald 1 Alagi, Gábor 1 Althaus, Ernst 1 Asperti, Andrea 1 Barrett, Clark W. 1 Beeson, Michael J. 1 Benzmüller, Christoph Ewald 1 Bigarella, Filippo 1 Bjørner, Nikolaj S. 1 Brauße, Franz 1 Bury, Guillaume 1 Cauderlier, Raphaël 1 Cimatti, Alessandro 1 Conchon, Sylvain 1 Danas, Ryan 1 Delahaye, David 1 Desharnais, Martin 1 Dolzmann, Andreas 1 Dougherty, Daniel J. 1 Dragoste, Irina 1 Dross, Claire 1 Dwyer, Matthew B. 1 Echenim, Mnacho 1 Faqeh, Rasha 1 Fetzer, Christof 1 Fietzke, Arnaud 1 Fiori, Alberto 1 Fröhlich, Andreas M. 1 Fu, Huimin 1 Garvin, Brady J. 1 Gauthier, Thibault 1 Ge-Ernst, Aile 1 Ghilardi, Silvio 1 Giese, Martin A. 1 Giesl, Jürgen 1 Graham-Lengrand, Stéphane 1 Griggio, Alberto 1 Halmagrand, Pierre 1 Hermant, Olivier 1 Holden, Edvard K. 1 Iosif, Radu 1 Irfan, Ahmed 1 Janičić, Predrag 1 Järvisalo, Matti 1 Ji, Kailiang 1 Jonáš, Martin 1 Kanig, Johannes 1 Kapur, Deepak 1 Khasidashvili, Zurab O. 1 King, Tim 1 Kinyon, Michael K. 1 Korovina, Margarita Vladimirovna 1 Košta, Marek 1 Kotel’nikov, Evgeny A. 1 Kovásznai, Gergely 1 Krötzsch, Markus 1 Kuncak, Viktor 1 Leidinger, Hendrik 1 Leutgeb, Lorenz 1 Manna, Zohar ...and 58 more Authors all top 5 Cited in 16 Serials 23 Journal of Automated Reasoning 3 Information and Computation 2 Journal of Symbolic Computation 2 Theory and Practice of Logic Programming 2 Mathematics in Computer Science 1 Artificial Intelligence 1 The Journal of Symbolic Logic 1 Theoretical Computer Science 1 AI Communications 1 MSCS. Mathematical Structures in Computer Science 1 Applicable Algebra in Engineering, Communication and Computing 1 Formal Methods in System Design 1 Annals of Mathematics and Artificial Intelligence 1 Theory of Computing Systems 1 ACM Transactions on Computational Logic 1 Symmetry all top 5 Cited in 6 Fields 96 Computer science (68-XX) 49 Mathematical logic and foundations (03-XX) 3 Operations research, mathematical programming (90-XX) 1 History and biography (01-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Group theory and generalizations (20-XX) Citations by Year