Programming and automating mathematics in the Tarski-Kleene hierarchy

DOI10.1016/j.jlap.2014.02.001zbMath1434.68637OpenAlexW2108356686MaRDI QIDQ406433

Alasdair Armstrong, Tjark Weber, Georg Struth

Publication date: 8 September 2014

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

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

zbMATH Keywords

relation algebrainteractive theorem provingKleene algebraformalised mathematics

Mathematics Subject Classification ID

Cylindric and polyadic algebras; relation algebras (03G15) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Developments in concurrent Kleene algebra ⋮ Convolution and concurrency ⋮ Completeness for Identity-free Kleene Lattices ⋮ Building program construction and verification tools from algebraic principles ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• Isabelle
• RelView
• Isabelle/HOL
• HOL
• Sledgehammer
• Regular Sets

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
• Relation algebras
• A completeness theorem for Kleene algebras and the algebra of regular events
• Dioïds and semirings: Links to fuzzy sets and other applications
• Proof Pearl: regular expression equivalence and relation algebra
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Automatic Proof and Disproof in Isabelle/HOL
• On Automating the Calculus of Relations
• Constructive Type Classes in Isabelle
• Computer Algebra in Scientific Computing
• Relational and Kleene-Algebraic Methods in Computer Science
• An Efficient Coq Tactic for Deciding Kleene Algebras
• Boolean Algebras with Operators. Part I
• Boolean Algebras with Operators
• Formal power series