Automated Reasoning in Kleene Algebra
From MaRDI portal
Publication:3608779
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
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Other algebras related to logic (03G25)
Cited In (38)
- Title not available (Why is that?)
- Modal Semirings Revisited
- A relation-algebraic approach to the ``Hoare logic of functional dependencies
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Dual choice and iteration in an abstract algebra of action
- 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
- Title not available (Why is that?)
- Non-termination in Idempotent Semirings
- Building program construction and verification tools from algebraic principles
- Algebraic separation logic
- Internal axioms for domain semirings
- Dijkstra, Floyd and Warshall meet Kleene
- Normal design algebra
- On the complexity of reasoning in Kleene algebra
- Enabledness and termination in refinement algebra
- Circulations, Fuzzy Relations and Semirings
- Automated verification of refinement laws
- Automated flaw detection in algebraic specifications
- Knowledge and Games in Modal Semirings
- Automating Coherent Logic
- Deciding Kleene algebra terms equivalence in Coq
- 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)\)
- Automated Reasoning in Higher-Order Regular Algebra
- Geographic wayfinders and space-time algebra
- Automated Reasoning for Hybrid Systems — Two Case Studies —
Uses Software
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)
