Abstract
Orientability of systems of equalities is the following problem: Given a system of equalities s1 ≃ t1, . . . , sn ≃ tn, does there exist a simplification ordering ≻ which orients the system, that is for every i ∈ {1,..., n}, either si ≻ ti or ti ≻ si. 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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - Symposium on Logic in Computer Science|Proc Symp Logic Comput Sci |
| Publisher | IEEE Computer Society |
| Pages | 75-84 |
| Number of pages | 9 |
| Publication status | Published - 2003 |
| Event | 18th Annual IEEE Symposium on Logic in Computer Science - Ottawa, Ont. Duration: 1 Jul 2003 → … http://ieeexplore.ieee.org/iel5/8592/27231/01210045.pdf?tp=&arnumber=1210045&isnumber=27231 |
Conference
| Conference | 18th Annual IEEE Symposium on Logic in Computer Science |
|---|---|
| City | Ottawa, Ont. |
| Period | 1/07/03 → … |
| Internet address |