| |

:: Home:: What is EACSL:: Organization:: Membership:: CSL Conferences:: Ackermann Award:: Alonzo Church Award:: CSL Bibliography:: Constitutions:: Minutes:: Contact |
## Ackermann Award 2005: Konstantin Korovin## CitationKonstantion Korovin recieves the 2005 Ackermann Award of the European Association of Computer Science Logic (EACSL) for his thesis## Knuth-Bendix orders in automated deduction and term rewriting.## Background of the thesisAutomated deduction is an important branch of Computer science, which has applications in various areas including specification and verfication of software and hardware, synthesis of safe programs, database systems, computer algebra and others. One of the most popular methods used in automated deduction are resolution based-theorem proving, which can be implemented efficiently, yet is powerful enough for many applications. Incorporated in the resolution method are various unification algorithms and term rewrite techniques. Because of the practical importance of resolution, unification and term rewriting, intensive research has been devoted both to theoretical improvements as well as implementation issues. Among the main tools developed for termination proofs and improved implementation strategies are orderings on term algebras, and the use of ordering restrictions, which allow to cut down the search space.
There are two classes of orderings that are widely used in
automated deduction:
In the
seminal 1970 paper by D. Knuth and P. Bendix
The first order theory of RPOs was
proven undecidable in 1992,
by R. Treinen,
and for LPOs
in 1997.
by H. Comon and R. Treinen.
In 2000 P. Narendran and M. Rusinowitch showed that
the first order theory of unary RPOs is decidable.
They also showed that
solving RPOs constraints is in NP in 1998.
It was known to be NP-hard since 1984.
There exists an extensive literature on RPOs and LPOs.
For a survey and historic details we refer to the handbook article
on Rewriting
by N. Dershowitz and D.A. Plaisted in
Although there have been many results on the properties of all variants of recursive path orderings, virtually nothing was known about the KBOs, before the work of K. Korovin, which was published jointly with his supervisor A. Voronkov. It seems the main problem with proving results about KBOs is the (non-trivial) combination of integers and term algebras, as compared to pure combinatorics on term algebras in the case of RPOs and KBOs. ## Korovin's thesisKonstantin Korovins thesis deals with the algorithmic properties of Knuth-Bendix orders. In his thesis, he has constructed polynomial time algorithms for the fundamental problems of solving ordering constraints of single inequalities, of the orientabilty of systems of equalities and rewrite rules by KBOs, and for term comparison. He has given lower bounds for the complexity of these problems showing that orientability is P-time complete, and the problem of solving ordering constraints is NP-complete. The general first order decision problem for KBOs is widely believed to be solvable, but no proof of this fact has been found so far. Korovin has shown the decidability of first ordering constraints for unary signatures. The proofs of the main results display a high level of interdisciplinarity, with a blend of optimization theory, complexity theory, and a mastery of a multitude of techniques for establishing effective decision procedures.## Biographic SketchKonstantin Korovin was born on April 4, 1976 in Sarapul, Russia (Soviet Union). He received his secondary education at the Specialized Scientific Study Center for Physics, Mathematics, Chemistry and Biology in Novosibirsk in the period from 1992-93. At the age of 17 he entered Novosibirsk University and received both his undergraduate and graduate education there. In 1998 he completed his M.Sc. studies under the supervision of Prof. Andrei Morozov. The title of his M.Sc. thesis is Compositions of
permutations and algorithmic reducibilities.
From 1999-2002 he was a Ph.D. student under the supervision of Prof.
Andrei Voronkov, and received his Ph.D. in 2003
for his thesis He spent the years 2003 and 2004 as a researcher at the Max Planck Institute in Saarbrucken, Germany, working with Professor Harald Ganzinger, in the difficult period when Ganzinger was already very ill and until his untimely death. He wrote several important papers with Harald Ganzinger, but it was his sole responsibility to elaborate, develope and complete Ganzinger's ideas. After Ganzinger's death he returned to Manchester University where he works as a research associate. |