Internal axioms for domain semirings
type: Item
instance of: scholarly article
title: Internal axioms for domain semirings
zbMATH Open document ID: 1211.68242
author: Jules Desharnais
author: Georg Struth
published in: Science of Computer Programming
publication date: 2011-02-21T00:00:00Z
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03G25
Mathematics Subject Classification ID: 16Y60
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5853825
zbMATH Keywords: semiring
zbMATH Keywords: Kleene algebra
zbMATH Keywords: modal semiring
zbMATH Keywords: domain operator
zbMATH Keywords: codomain operator
zbMATH Keywords: antidomain operator
zbMATH Keywords: algebra of domain elements
zbMATH Keywords: distributive lattice
zbMATH Keywords: Boolean algebra
zbMATH Keywords: Heyting algebra
zbMATH Keywords: Löb's formula
zbMATH Keywords: automated theorem proving
describes a project that uses: Mace4
describes a project that uses: Waldmeister
describes a project that uses: TPTP
describes a project that uses: Prover9
MaRDI profile type: Publication
full work available at URL: j.scico.2010.05.007
OpenAlex ID: W2001616837
cites work: Q5331549
cites work: Algebraizable logics
cites work: Q5437872
cites work: Q4673439
cites work: Kleene algebra with domain
cites work: Domain Axioms for a Family of Near-Semirings
cites work: Modal Semirings Revisited
cites work: Theory Is Forever
cites work: Automated Reasoning in Kleene Algebra
cites work: Automated verification of refinement laws
cites work: The Structure of the One-Generated Free Domain Semiring
cites work: Q3965241
cites work: Boolean Algebras with Operators. Part I
cites work: A completeness theorem for Kleene algebras and the algebra of regular events
cites work: Q4362921
cites work: Kleene modules and linear languages
cites work: Computer Science Logic
cites work: Algebras of modal operators and partial correctness
cites work: Automated theorem proving by resolution in non-classical logics
cites work: Modal Tools for Separation and Refinement
cites work: Automated Reasoning
cites work: The TPTP problem library. CNF release v1. 2. 1
cites work: Towards a refinement algebra
DOI: 10.1016/J.SCICO.2010.05.007
description: scientific article; zbMATH DE number 5853825