Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template :: Thesis :: Korovin, Konstantin


Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit


Author
Author(s)*:Korovin, Konstantin
BibTeX citekey*:KorovinPhD2003
Language:English

Title, School
Title*:{Knuth-Bendix} orders in automated deduction and term rewriting
School:University of Manchester
Type of Thesis*:Doctoral dissertation
Month:November
Year:2003


Note, Abstract, Copyright
LaTeX Abstract:Ordering restrictions play a crucial role in automated deduction.

In particular, orders are used extensively
for pruning search space in automated theorem provers and
for rewriting-based reasoning and computation.
There are two classes of orders that are widely used
in automated deduction: Knuth-Bendix orders and various versions of recursive path orders.
Despite the fact that Knuth-Bendix orders
were discovered earlier than recursive path orders, and since then have been used in many state-of-the-art automated theorem provers; the decidability and complexity of many important problems related to these orders remained open.
In this thesis we try to close this gap
and provide various decidability and complexity results
for a number of important decision problems related to Knuth-Bendix orders.
We prove the decidability and NP-completeness of
the problem of solving Knuth-Bendix ordering constraints.
In the case of constraints consisting of single
inequalities we present a polynomial-time algorithm.
We also prove the decidability of the problem of solving
general first-order Knuth-Bendix ordering constraints
over unary signatures.
Another problem we study is the orientability
problem by Knuth-Bendix orders.
We present a polynomial-time algorithm for orientability
of systems consisting of term rewrite rules and equalities by Knuth-Bendix orders, and prove that this problem is P-complete.
Finally, we show that it is possible to extend Knuth-Bendix orders to AC-compatible orders preserving attractive properties of Knuth-Bendix orders.

Download Access Level:Public
Download File(s):

Referees, Status, Dates
1. Referee:Professor Peter Aczel
2. Referee:Professor Robert Nieuwenhuis
Supervisor:Professor Andrei Voronkov
Status:Completed
Date Kolloquium:22 January 2004

Correlation
MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort


BibTeX Entry:
@PHDTHESIS{KorovinPhD2003,
AUTHOR = {Korovin, Konstantin},
TITLE = {{Knuth-Bendix} orders in automated deduction and term rewriting},
SCHOOL = {University of Manchester},
YEAR = {2003},
TYPE = {Doctoral dissertation}
MONTH = {November},
}





Entry last modified by Anja Becker, 01/28/2008
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Konstantin Korovin
Created
01/22/2004 08:29:22 PM
Revisions
3.
2.
1.
0.
Editor(s)
Anja Becker
Christine Kiesel
Christine Kiesel
Konstantin Korovin
Edit Dates
21.06.2004 16:08:28
17.06.2004 18:03:53
17.06.2004 16:20:14
01/22/2004 08:29:22 PM