Abstract
We show that the first-order theory of any Knuth-Bendix order in the case of the signatures consisting of unary function symbols and constants is decid-able. Our decision procedure uses interpretation of unary terms as trees and uses decidability of the weak monadic second-order theory of binary trees. One area of applications of our result is automated deduction, since using the first-order theory of the Knuth-Bendix orders we can decide an important class of ordering constraints. © Springer-Verlag Berlin Heidelberg 2002.
| Original language | English |
|---|---|
| Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci. |
| Publisher | Springer Nature |
| Pages | 230-240 |
| Number of pages | 10 |
| Volume | 2556 |
| ISBN (Print) | 3540002251, 9783540002253 |
| Publication status | Published - 2002 |
| Event | 22nd International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2002 - Kanpur Duration: 1 Jul 2002 → … http://dblp.uni-trier.de/db/conf/fsttcs/fsttcs2002.html#KorovinV02http://dblp.uni-trier.de/rec/bibtex/conf/fsttcs/KorovinV02.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/fsttcs/KorovinV02 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|
Conference
| Conference | 22nd International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2002 |
|---|---|
| City | Kanpur |
| Period | 1/07/02 → … |
| Internet address |