KOROVIN, KONSTANTIN

KOROVIN, KONSTANTIN

E-mail : korovin (AT) cs.man.ac.uk

Research Associate,
School of Computer Science, The University of Manchester,
Manchester, UK.

Research Interests :
Logic in Computer Science:
* Solving constraints in term algebras
* Instantiation-based theorem proving
* Automated deduction
* Complexity Theory

Logic:
* Computability Theory
* Model Theory

Awards and Honors :
2005 Ackermann Award of the European Association of Computer Science Logic (EACSL) for his thesis "Knuth-Bendix orders in automated deduction and term rewriting"

Selected Publications :
Theory Instantiation, H. Ganzinger, K. Korovin LPAR'06 ©Springer-Verlag,

Random Databases and Threshold for Monotone Non-Recursive Datalog, K. Korovin, A. Voronkov
MFCS'05, ©Springer-Verlag,

Integrating equational reasoning into instantiation-based theorem proving, H. Ganzinger, K. Korovin
CSL'04, ©Springer-Verlag,

New Directions in Instantiation-Based Theorem Proving, H. Ganzinger, K. Korovin
LICS'03, ©IEEE,

Orienting Equalities with the Knuth-Bendix Order, K. Korovin, A. Voronkov
LICS'03, ©IEEE,

An AC-Compatible Knuth-Bendix Order, K. Korovin, A. Voronkov
CADE'03, ©Springer-Verlag

The decidability of the first-order theory of the Knuth-Bendix order in the case of unary signatures, K. Korovin, A. Voronkov
FSTTCS'02, ©Springer-Verlag,

Verifying orientability of rewrite rules using the Knuth-Bendix order, K. Korovin, A. Voronkov
RTA'01, ©Springer-Verlag, journal version has appeared in Information and Computation.

Knuth-Bendix constraint solving is NP-complete, K. Korovin, A. Voronkov
ICALP'01, ©Springer-Verlag journal version is to appear in ACM Transactions on Computational Logic.

A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering, K. Korovin, A. Voronkov
LICS'00, ©IEEE

Compositions of permutations and algorithmic reducibilities, K. Korovin
in Recursion Theory and Complexity, de Gruyter Series in Logic and Applications 2, pp89-95, 1999.