A formal proof system for infinitary rational expressions. (English) Zbl 0575.68083

Automata on infinite words, Ec. Printemps Inf. Théor., Le Mont Dore 1984, Lect. Notes Comput. Sci. 192, 68-80 (1985).
[For the entire collection see Zbl 0563.00019.]
In his classical work [Theory of automata (1969; Zbl 0193.329)], A. Salomaa supplies a sound and complete axiom system for testing the equality of rational languages, using the free word algebra of rational expressions. This paper does the same thing for \(\omega\)-rational languages (\(\omega\)-rational expressions). Despite its complexity the system is carefully and gradually constructed. It parallels the known decision procedure for testing the equality of \(\omega\)-languages and it essentially uses not only \(''=''\) but also some additional predicate symbols.
Reviewer: C.Masalagiu


68Q45 Formal languages and automata
03D05 Automata and formal grammars in connection with logical questions
68Q65 Abstract data types; algebraic specification
03B25 Decidability of theories and sets of sentences