The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable.
Konstantin Korovin, Андрей Воронков · 2000
s a sum of weights of functors occurring in the term. Given a weight function w and a linear ordering AE on \\Sigma, the Knuth-Bendix ordering on TA(\\Sigma) is the binary relation ?KB defined as follows. For any ground terms g(t 1 ; : : : ; t n ) and h(s 1 ; : : : ; s k ) we have g(t 1 ; : : : ; t n ) ?KB h(s 1 ; : : : ; s k ) if 1. jg(t 1 ; : : : ; t n )j ? jh(s 1 ; : : : ; s k )j or 2. jg(t 1 ; : : : ; t n )j = jh(s 1<