Some undecidability results for non-monadic Church-Rosser Thue systems (Q1057264)

A linear sentence on the alphabet A is a string of the form \(\forall u_ 1...\forall u_ m\exists v_ 1...\exists v_ nF\) or \(\exists v_ 1...\exists v_ n\forall u_ 1...\forall u_ mF\) where \(u_ i\in V_ u\), the set of universal variables, \(v_ i\in V_ E\), the set of existential variables and F has one of the forms \(x\sim y\) (x,y\(\in (A\cup V_ u)^*\cup (A\cup V_ E)^*)\), \(F_ 1\wedge F_ 2\), or \(F_ 1\vee F_ 2\) and no variable occurs twice in F. A Thue system on A defines an interpretation of the linear sentences on A by taking the congruence relation for \(\sim\). It is known that there is an algorithm which decides whether a linear sentence on A is true or not under the interpretation given by a monadic finite Thue system on A that is Church- Rosser. In the paper the case of non-monadic finite Thue systems that are Church-Rosser is considered. The main result claims that it is undecidable whether a linear sentence on A is true or not under the interpretation given by a non-monadic finite Thue system on A that is Church-Rosser. Some problems that are decidable for monadic Church-Rosser Thue systems but that are undecidable for non-monadic Church-Rosser Thue systems are presented.