{Knuth-Bendix} orders in automated deduction and term rewriting

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.

January

2004