Programming and automating mathematics in the Tarski-Kleene hierarchy

DOI10.1016/J.JLAP.2014.02.001MaRDI QIDQ406433zbMATH OpenOpenAlexFDO

Authors Alasdair Armstrong, Georg Struth, Tjark Weber

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)

Recommendations

• Mathematical programming: Turing completeness and applications to software analysis
• Automated Reasoning in Kleene Algebra
• Symbolic computation in automated program reasoning
• Finite automata in the mathematical theory of programming
• Automatic Proof Generation in Kleene Algebra
• scientific article; zbMATH DE number 3890767
• Program algebra for Turing-machine programs
• scientific article; zbMATH DE number 140006
• A generalized mathematical theory of structured programming
• scientific article; zbMATH DE number 978243

Cites work

• scientific article; zbMATH DE number 4210141 (Why is no real title available?)
• scientific article; zbMATH DE number 41838 (Why is no real title available?)
• scientific article; zbMATH DE number 549971 (Why is no real title available?)
• A completeness theorem for Kleene algebras and the algebra of regular events
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings
• An efficient Coq tactic for deciding Kleene algebras
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Automatic proof and disproof in Isabelle/HOL
• Boolean Algebras with Operators
• Boolean Algebras with Operators. Part I
• Computer Algebra in Scientific Computing
• Constructive Type Classes in Isabelle
• Dioïds and semirings: Links to fuzzy sets and other applications
• Formal power series
• Internal axioms for domain semirings
• On Automating the Calculus of Relations
• Proof Pearl: regular expression equivalence and relation algebra
• Relation algebras
• Relational and Kleene-Algebraic Methods in Computer Science
• Relational mathematics

Cited in

(7)

• Automated Reasoning in Kleene Algebra
• Convolution and concurrency
• Developments in concurrent Kleene algebra
• Building program construction and verification tools from algebraic principles
• Modelling algebraic structures and morphisms in ACL2
• scientific article; zbMATH DE number 65747 (Why is no real title available?)
• Completeness for identity-free Kleene lattices

Describes a project that uses

Uses Software

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

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)