:: Home
:: What is EACSL
:: Organization
:: Membership
:: CSL Conferences
:: Ackermann Award
:: Alonzo Church Award
:: CSL Bibliography
:: Constitutions
:: Minutes
:: Contact

Ackermann Award 2005: Konstantin Korovin


Konstantion 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

In this thesis he has advanced single-handedly the theoretical and algorithmic foundations of Knuth-Bendix orderings, separating effectively the feasible applicabilty of Knuth-Bendix orderings from its less feasible aspects.

Background of the thesis

Automated 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 Simple word problems in universal algebra, Knuth-Bendix Orderings (KBOs), were introduced. Knuth-Bendix orders have a hybrid nature. They are defined on weighted terms of term algebras, relying both on syntactic precedence and a numeric weight function, hence introducing a (non-trivial) combination of integers and terms. In 1979, N. Dershowitz introduced recursive path orderings (RPOs) for the same purpose. Recursive path orders are defined on term algebras, relying on syntactic precendence only, without weights. The literature is rich in variations of the concept of RPOs. A popular variant are the lexicographical path orderings (LPOs) introduced by Levy and Kamin in 1980. Both types of term orderings are are widely used in almost all currently implemented and widely used automated theorem provers. Knuth-Bendix orderings (KBOs) is the main family of orderings used in the theorem provers VAMPIR, E, Waldmeister, and SPASS.

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 Handbook of Automated Reasoning, edited by A. Robinson and A. Voronkov, MIT Press and Elsevier, 2001.

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 thesis

Konstantin 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 Sketch

Konstantin 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 Knuth-Bendix orders in automated deduction and term rewriting. For this thesis he already received the best Ph.D. Thesis Award of the University of Manchester.

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.