| iProver–an instantiation-based theorem prover for first-order logic (system description) K Korovin International Joint Conference on Automated Reasoning, 292-298, 2008 | 237 | 2008 |
| New directions in instantiation-based theorem proving H Ganzinger, K Korovin 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings …, 2003 | 138 | 2003 |
| Inst-Gen – A modular approach to instantiation-based reasoning. K Korovin Programming Logics - Essays in Memory of Harald Ganzinger. 7797 (LNCS), 239-270, 2013 | 86 | 2013 |
| Integrating linear arithmetic into superposition calculus K Korovin, A Voronkov Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual …, 2007 | 69 | 2007 |
| An invitation to instantiation-based reasoning: From Theory to Practice K Korovin Automated Deduction–CADE-22, 163-166, 2009 | 60* | 2009 |
| Conflict resolution K Korovin, N Tsiskaridze, A Voronkov International Conference on Principles and Practice of Constraint …, 2009 | 57 | 2009 |
| Computing exponentially faster: implementing a non-deterministic universal Turing machine using DNA A Currin, K Korovin, M Ababi, K Roper, DB Kell, PJ Day, RD King Journal of the Royal Society Interface 14 (128), 20160990, 2017 | 50 | 2017 |
| Integrating equational reasoning into instantiation-based theorem proving H Ganzinger, K Korovin Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual …, 2004 | 46 | 2004 |
| Theory instantiation H Ganzinger, K Korovin International Conference on Logic for Programming Artificial Intelligence …, 2006 | 44 | 2006 |
| Orienting rewrite rules with the Knuth–Bendix order K Korovin, A Voronkov Information and Computation 183 (2), 165-186, 2003 | 36 | 2003 |
| Implementing superposition in iProver (system description) A Duarte, K Korovin Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris …, 2020 | 34 | 2020 |
| An invitation to instantiation-based reasoning reasoning: From Theory to Practice K Korovin Proceedings of the 22nd International Conference on Automated Deduction, 2008 | 34* | 2008 |
| iProver-Eq: An instantiation-based theorem prover with equality K Korovin, C Sticksel Automated Reasoning: 5th International Joint Conference, IJCAR 2010 …, 2010 | 33 | 2010 |
| Encoding industrial hardware verification problems into effectively propositional logic M Emmer, Z Khasidashvili, K Korovin, A Voronkov Formal Methods in Computer Aided Design, 137-144, 2010 | 31 | 2010 |
| Knuth-Bendix constraint solving is NP-complete K Korovin, A Voronkov Automata, Languages and Programming: 28th International Colloquium, ICALP …, 2001 | 31* | 2001 |
| A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering K Korovin, A Voronkov Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science …, 2000 | 31 | 2000 |
| Non-cyclic sorts for first-order satisfiability K Korovin Frontiers of Combining Systems: 9th International Symposium, FroCoS 2013 …, 2013 | 25 | 2013 |
| Preprocessing techniques for first-order clausification K Hoder, Z Khasidashvili, K Korovin, A Voronkov 2012 Formal Methods in Computer-Aided Design (FMCAD), 44-51, 2012 | 24 | 2012 |
| Heterogeneous heuristic optimisation and scheduling for first-order theorem proving EK Holden, K Korovin International Conference on Intelligent Computer Mathematics, 107-123, 2021 | 23 | 2021 |
| Solving systems of linear inequalities by bound propagation K Korovin, A Voronkov International Conference on Automated Deduction, 369-383, 2011 | 21 | 2011 |
Andrei VoronkovThe University of Manchester; EasyChair在 cs.man.ac.uk 的电子邮件经过验证
