Automated Reasoning in Kleene Algebra

DOI10.1007/978-3-540-73595-3_19zbMath1184.68462OpenAlexW1762364904MaRDI QIDQ3608779

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

Related Items (29)

An algebraic approach to computations with progress ⋮ Normal design algebra ⋮ Deciding Regular Expressions (In-)Equivalence in Coq ⋮ Algebraic notions of nontermination: Omega and divergence in idempotent semirings ⋮ Automated Reasoning for Hybrid Systems — Two Case Studies — ⋮ Non-termination in Idempotent Semirings ⋮ Knowledge and Games in Modal Semirings ⋮ A relation-algebraic approach to the ``Hoare logic of functional dependencies ⋮ Geographic wayfinders and space-time algebra ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Internal axioms for domain semirings ⋮ Dijkstra, Floyd and Warshall meet Kleene ⋮ Circulations, Fuzzy Relations and Semirings ⋮ Modal Semirings Revisited ⋮ Enabledness and termination in refinement algebra ⋮ Algebraic neighbourhood logic ⋮ A sketch of a dynamic epistemic semiring ⋮ Dual choice and iteration in an abstract algebra of action ⋮ Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) ⋮ Fixing Zeno gaps ⋮ Algebraic separation logic ⋮ Normal forms in total correctness for while programs and action systems ⋮ An algebra of hybrid systems ⋮ Building program construction and verification tools from algebraic principles ⋮ Automated verification of refinement laws ⋮ Denotation by Transformation ⋮ Modal algebra and Petri nets ⋮ Extended transitive separation logic ⋮ Deciding Kleene algebra terms equivalence in Coq

Uses Software

• Prover9
• Mace4

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