Programming and automating mathematics in the Tarski-Kleene hierarchy
From MaRDI portal
Publication:406433
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
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
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