Left omega algebras and regular equations

Left omega algebras, where one of the usual star induction axioms is absent, are studied in the context of recursive regular equations. Abstract conditions for explicitly defining the omega operation are presented. They are used for developing abstract side conditions on Arden’s rule that are necessary for solving such equations. The definability and solvability results are refined to concrete models, to languages, traces and relations. It turns out, for instance, that the omega operation captures precisely the empty word property in regular languages and wellfoundedness in relational models. The approach also leads to simple new relative completeness results for left omega algebras, and for Salomaa’s axioms for regular expressions. Since automated theorem proving and counterexample search within the theorem proving environment Isabelle/HOL are instrumental for this investigation, it is also an exercise in formalised mathematics.