Left omega algebras and regular equations

DOI10.1016/j.jlap.2012.05.004zbMath1279.68242MaRDI QIDQ1931903

Georg Struth

Publication date: 16 January 2013

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2012.05.004

zbMATH Keywords

formalised mathematics; regular equations; Arden's rule; automated and interactive theorem proving; Kleene and omega algebra

Mathematics Subject Classification ID

68Q70: Algebraic theory of languages and automata

Related Items

Taming Multirelations, Automated Reasoning in Higher-Order Regular Algebra

Uses Software

• Isabelle/HOL
• Sledgehammer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings
• Internal axioms for domain semirings
• A completeness theorem for Kleene algebras and the algebra of regular events
• A calculational approach to mathematical induction
• Isabelle/HOL. A proof assistant for higher-order logic
• Automated Analysis of Regular Algebra
• Algebraic Notions of Termination
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Automatic Proof and Disproof in Isabelle/HOL
• Regular Algebra Applied to Path-finding Problems
• Une condition impliquant toutes les identités rationnelles
• Two Complete Axiom Systems for the Algebra of Regular Events