Dear Jens,

Canonic (i.e., confluent and terminating) TRS's indeed provide a

decision procedure for their corresponding equational theories. Yet

these equational theories are not usually complete, but only

ground-complete for the intended model. (I am probably not using

standard terminology here.) For example, take the usual euqations that

define multiplication and addition in terms of 0 and successor:

x + 0 = x

x + S y = S(x + y)

x * 0 = 0

x * S y = x * y + x

This system is confluent and terminating for ground terms (by ground

term I mean term not containing variables), implying

decidability of the ground identities (i.e., of the form t1 = t2 with

t1 and t2 ground terms) which are (syntactic) consequences of that

theory. And, via ground completeness, these identities are the same

as the ones true in the algebra of natural numbers, so we have a

decision procedure for ground identities on natural numbers with 0, S,

+, *.

The same line of reasoning cannot be applied to arbitrary equations

though, because, while the above system if confluent and terminating

on arbitrary terms too, it is not true that the corresponding

equations are enough to deduce syntactically all true equations about

numbers. (E.g., associativity of + does not follow using the

equational deduction system.)

Summing up the above discussion, a canonical TRS of the form you have

in mind does make its own equational theory decidable, but that

equational theory needs not be complete for the intended model.

On the other hand, there are techniques more powerful than TRS

canonicity (about which I know very little) that ensure decidability

of the equational theory of a fixed model, such as that of the

naturals. Your question made me curious and I have searched for the

answer to the decidability problem

for the equational theory of naturals -- please find at the link below

an article that I found, containing a positive answer for the case

of addition, multiplication and exponentiation.

http://www.springerlink.com/content/g7lwvhbdcw7xbh59/
Best regards,

Andrei

--- In univalg@yahoogroups.com, "Jens Doll" <jd@...> wrote:

>

> Hello Andrei,

>

> consider a grammar G, which generates terms T and also consider

> equations E out of language L(G), which together with G define a

> terminating and confluent TRS and enable me to reduce each sentence

> from L(G) to a normal form N.

>

> What is the normal form N for? I suppose, one could define a set of

> equations and a normal form N, so that you can derive from the reduced

> sentence, if it belongs to the class of true aritmetic formulas or not.

>

> Jens

>