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
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
- A generalized mathematical theory of structured programming
- scientific article; zbMATH DE number 978243
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
- 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
- Title not available (Why is that?)
- A completeness theorem for Kleene algebras and the algebra of regular events
- Title not available (Why is that?)
- Title not available (Why is that?)
- Internal axioms for domain semirings
- Title not available (Why is that?)
- 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 (7)
- Automated Reasoning in Kleene Algebra
- 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
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)
