Chercheurs

Informatique / KOROVIN, KONSTANTIN

korovin

Position

University Research Fellow and Lecturer at School of Computer Science, The University of Manchester,
Manchester, UK.

Thèmes de recherche

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

Logic:
* Computability Theory
* Model Theory

Prix et récompenses

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

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.