# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Orienting Equalities with the Knuth-Bendix Order

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Korovin, K., & Voronkov, A. (2003). Orienting Equalities with the Knuth-Bendix
Order. In *18th Annual IEEE Symposium on Logic in Computer Science (LICS-03)* (pp. 75-84).
Los Alamitos, USA: IEEE.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2DB0-9

##### Abstract

Orientability of systems of equalities is the following
problem: given a system of equalities $s_1 \eql t_1, \ldots,
s_n \eql t_n$, does there exist a simplification ordering $\succ$
which orients the system,
that is for every $i \in \{1,...,n\}$,
either $s_i \succ t_i$ or $t_i \succ s_i$.
This problem can be used in rewriting for finding
a canonical rewrite system for a system of equalities
and in theorem proving for adjusting simplification
orderings during completion. We prove that (rather surprisingly)
the problem can be solved in polynomial time when we restrict ourselves to the
Knuth-Bendix orderings.