Follow
Konstantin Korovin
Konstantin Korovin
University of Manchester, School of Computer Science
Verified email at manchester.ac.uk - Homepage
Title
Cited by
Cited by
Year
iProver–an instantiation-based theorem prover for first-order logic (system description)
K Korovin
International Joint Conference on Automated Reasoning, 292-298, 2008
2322008
New directions in instantiation-based theorem proving
H Ganzinger, K Korovin
18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings …, 2003
1352003
Inst-Gen – A modular approach to instantiation-based reasoning.
K Korovin
Programming Logics - Essays in Memory of Harald Ganzinger. 7797 (LNCS), 239-270, 2013
852013
Integrating linear arithmetic into superposition calculus
K Korovin, A Voronkov
Computer Science Logic: 21st International Workshop, CSL 2007, 16th Annual …, 2007
692007
An invitation to instantiation-based reasoning: From Theory to Practice
K Korovin
Automated Deduction–CADE-22, 163-166, 2009
59*2009
Conflict resolution
K Korovin, N Tsiskaridze, A Voronkov
International Conference on Principles and Practice of Constraint …, 2009
542009
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
492017
Integrating equational reasoning into instantiation-based theorem proving
H Ganzinger, K Korovin
Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual …, 2004
452004
Theory instantiation
H Ganzinger, K Korovin
International Conference on Logic for Programming Artificial Intelligence …, 2006
432006
Implementing superposition in iProver (system description)
A Duarte, K Korovin
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris …, 2020
352020
Orienting rewrite rules with the Knuth–Bendix order
K Korovin, A Voronkov
Information and Computation 183 (2), 165-186, 2003
352003
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
332010
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
312000
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
292010
Non-cyclic sorts for first-order satisfiability
K Korovin
Frontiers of Combining Systems: 9th International Symposium, FroCoS 2013 …, 2013
262013
An invitation to instantiation-based reasoning: from theory to practice
K Korovin
Volume in Memoriam of Harald Ganzinger 5663, 163-166, 2009
252009
An invitation to instantiation-based reasoning: from theory to practice
K Korovin
Volume in Memoriam of Harald Ganzinger 5663, 163-166, 2009
252009
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
242012
The system can't perform the operation now. Try again later.
Articles 1–20