Automated Reasoning in Kleene Algebra

DOI10.1007/978-3-540-73595-3_19zbMATH Open1184.68462OpenAlexW1762364904MaRDI QIDQ3608779FDOQ3608779

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

(38)

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

Describes a project that uses

Uses Software

• Prover9
• Mace4

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)