Konstantin Korovin
Citation
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.