Automated Reasoning in Kleene Algebra

DOI10.1007/978-3-540-73595-3_19MaRDI QIDQ3608779zbMATH OpenOpenAlexFDO

Authors Peter Höfner, Georg Struth

Publication date 6 March 2009

Published in Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73595-3_19

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other algebras related to logic (03G25)

Recommendations

• Programming and automating mathematics in the Tarski-Kleene hierarchy
• Modal Kleene algebra applied to program correctness
• Automated Reasoning for Hybrid Systems — Two Case Studies —
• Concurrent Kleene Algebra
• Automatic Proof Generation in Kleene Algebra

Cited in

(40)

• Modal Semirings Revisited
• scientific article; zbMATH DE number 978243 (Why is no real title available?)
• A relation-algebraic approach to the ``Hoare logic of functional dependencies
• Dual choice and iteration in an abstract algebra of action
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings
• A sketch of a dynamic epistemic semiring
• Fixing Zeno gaps
• Normal forms in total correctness for while programs and action systems
• An algebra of hybrid systems
• Extended transitive separation logic
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• An algebraic approach to computations with progress
• Programming and automating mathematics in the Tarski-Kleene hierarchy
• Building program construction and verification tools from algebraic principles
• Algebraic separation logic
• Non-termination in Idempotent Semirings
• scientific article; zbMATH DE number 6316277 (Why is no real title available?)
• Internal axioms for domain semirings
• Dijkstra, Floyd and Warshall meet Kleene
• Normal design algebra
• Enabledness and termination in refinement algebra
• On the complexity of reasoning in Kleene algebra
• Automated verification of refinement laws
• Circulations, Fuzzy Relations and Semirings
• Automated flaw detection in algebraic specifications
• Knowledge and Games in Modal Semirings
• Domain reasoning in TopKAT
• Deciding Kleene algebra terms equivalence in Coq
• Automating Coherent Logic
• Automated deduction with associative-commutative operators
• Denotation by Transformation
• Deciding regular expressions (in-)equivalence in Coq
• Modal algebra and Petri nets
• Algebraic neighbourhood logic
• Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\)
• Some uses of modal semirings
• Automated Reasoning in Higher-Order Regular Algebra
• Geographic wayfinders and space-time algebra
• Automated Reasoning for Hybrid Systems — Two Case Studies —

Describes a project that uses

Uses Software

• Mace4
• Prover9

This page was built for publication: Automated Reasoning in Kleene Algebra

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