Internal axioms for domain semirings

DOI10.1016/j.scico.2010.05.007zbMath1211.68242OpenAlexW2001616837MaRDI QIDQ627202

Georg Struth, Jules Desharnais

Publication date: 21 February 2011

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.05.007

zbMATH Keywords

Boolean algebradistributive latticeHeyting algebraautomated theorem provingsemiringKleene algebraalgebra of domain elementsantidomain operatorcodomain operatordomain operatorLöb's formulamodal semiring

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Other algebras related to logic (03G25) Semirings (16Y60)

Related Items

Concurrent Dynamic Algebra, Stone Relation Algebras, Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL, Developments in concurrent Kleene algebra, Algebraic coherent confluence and higher globular Kleene algebras, Unifying Lazy and Strict Computations, Automated Reasoning in Higher-Order Regular Algebra, A Hierarchy of Algebras for Boolean Subsets, Left omega algebras and regular equations, Programming and automating mathematics in the Tarski-Kleene hierarchy, Relational style laws and constructs of linear algebra, Catoids and modal convolution algebras, Embedding Kozen-Tiuryn logic into residuated one-sorted Kleene algebra with tests, On the complexity of Kleene algebra with domain, Relational Models for the Lambek Calculus with Intersection and Constants, On the expressive power of Kleene algebra with domain, \( \ell r\)-multisemigroups, modal quantales and the origin of locality, Abstract strategies and coherence, Free Kleene algebras with domain, Ordered domain algebras, How to generalise demonic composition, Hoare Semigroups, Verifying minimum spanning tree algorithms with Stone relation algebras, Fixpoints for general correctness, Algebras for iteration and infinite computations, Building program construction and verification tools from algebraic principles

Uses Software

• TPTP
• Prover9
• Mace4
• Waldmeister

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Kleene modules and linear languages
• Algebras of modal operators and partial correctness
• Automated verification of refinement laws
• The TPTP problem library. CNF release v1. 2. 1
• A completeness theorem for Kleene algebras and the algebra of regular events
• Towards a refinement algebra
• Automated theorem proving by resolution in non-classical logics
• The Structure of the One-Generated Free Domain Semiring
• Modal Semirings Revisited
• Automated Reasoning in Kleene Algebra
• Algebraizable logics
• Kleene algebra with domain
• Automated Reasoning
• Computer Science Logic
• Modal Tools for Separation and Refinement
• Domain Axioms for a Family of Near-Semirings
• Boolean Algebras with Operators. Part I
• Theory Is Forever