Programming and automating mathematics in the Tarski-Kleene hierarchy

DOI10.1016/J.JLAP.2014.02.001zbMATH Open1434.68637OpenAlexW2108356686MaRDI QIDQ406433FDOQ406433

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

interactive theorem provingrelation algebraKleene algebraformalised mathematics

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic Proof and Disproof in Isabelle/HOL
• Computer Algebra in Scientific Computing
• Dioïds and semirings: Links to fuzzy sets and other applications
• Boolean Algebras with Operators. Part I
• Boolean Algebras with Operators
• Relation algebras
• A completeness theorem for Kleene algebras and the algebra of regular events
• Internal axioms for domain semirings
• Proof Pearl: regular expression equivalence and relation algebra
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• On Automating the Calculus of Relations
• Constructive Type Classes in Isabelle
• Relational and Kleene-Algebraic Methods in Computer Science
• An Efficient Coq Tactic for Deciding Kleene Algebras
• Formal power series
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings

Cited In (6)

• Convolution and concurrency
• Developments in concurrent Kleene algebra
• Building program construction and verification tools from algebraic principles
• Completeness for Identity-free Kleene Lattices
• Title not available (Why is that?)
• Modelling algebraic structures and morphisms in ACL2

Uses Software

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

   Recommendations

• Mathematical programming: Turing completeness and applications to software analysis 👍 👎
• Automated Reasoning in Kleene Algebra 👍 👎
• Symbolic computation in automated program reasoning 👍 👎
• Title not available (Why is that?) 👍 👎
• Automatic Proof Generation in Kleene Algebra 👍 👎
• Title not available (Why is that?) 👍 👎
• Program Algebra for Turing-Machine Programs 👍 👎
• Title not available (Why is that?) 👍 👎
• A generalized mathematical theory of structured programming 👍 👎
• Title not available (Why is that?) 👍 👎

This page was built for publication: Programming and automating mathematics in the Tarski-Kleene hierarchy

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q406433)