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


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


Zbl 0476.00025