## The power of the Church-Rosser property for string rewriting systems.(English)Zbl 0535.68011

Automated deduction, 6th Conf., New York 1982, Lect. Notes Comput. Sci. 138, 360-368 (1982).
[For the entire collection see Zbl 0476.00025.]
The author studies finite monadic Church-Rosser Thue systems and he gives a decision procedure for a class of true sentences about Church-Rosser congruences. The class of sentences is defined syntactically and has prenex form $$\exists^ p\forall^ q$$ or $$\forall^ p\exists^ q$$, linear terms, positive matrices and other restrictions.
Reviewer: A.Pettorossi

### MSC:

 68Q65 Abstract data types; algebraic specification 03D03 Thue and Post systems, etc.

Zbl 0476.00025