View in EDS

Internal axioms for domain semirings

Saved in:
Bibliographic Details
Title: Internal axioms for domain semirings
Authors: Desharnais, Jules1 Jules.Desharnais@ift.ulaval.ca, Struth, Georg2 g.struth@dcs.shef.ac.uk
Source: Science of Computer Programming. Mar2011, Vol. 76 Issue 3, p181-203. 23p.
Subjects: Axioms, Semirings (Mathematics), Kleene algebra, Automatic theorem proving, Distributive lattices, Boolean algebra
Abstract: Abstract: New axioms for domain operations on semirings and Kleene algebras are proposed. They generalise the relational notion of domain–the set of all states that are related to some other state–to a wide range of models. They are internal since the algebras of state spaces are induced by the domain axioms. They are simpler and conceptually more appealing than previous two-sorted external approaches in which the domain algebra is determined through typing. They lead to a simple and natural algebraic approach to modal logics based on equational reasoning. The axiomatisations have been developed in a new style of computer-enhanced mathematics by automated theorem proving, and the approach itself is suitable for automated systems analysis and verification. This is demonstrated by a fully automated proof of a modal correspondence result for Löb’s formula that has applications in termination analysis. [ABSTRACT FROM AUTHOR]
Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 57369021
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Internal axioms for domain semirings
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Desharnais%2C+Jules%22">Desharnais, Jules</searchLink><relatesTo>1</relatesTo><i> Jules.Desharnais@ift.ulaval.ca</i><br /><searchLink fieldCode="AR" term="%22Struth%2C+Georg%22">Struth, Georg</searchLink><relatesTo>2</relatesTo><i> g.struth@dcs.shef.ac.uk</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Science+of+Computer+Programming%22">Science of Computer Programming</searchLink>. Mar2011, Vol. 76 Issue 3, p181-203. 23p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Axioms%22">Axioms</searchLink><br /><searchLink fieldCode="DE" term="%22Semirings+%28Mathematics%29%22">Semirings (Mathematics)</searchLink><br /><searchLink fieldCode="DE" term="%22Kleene+algebra%22">Kleene algebra</searchLink><br /><searchLink fieldCode="DE" term="%22Automatic+theorem+proving%22">Automatic theorem proving</searchLink><br /><searchLink fieldCode="DE" term="%22Distributive+lattices%22">Distributive lattices</searchLink><br /><searchLink fieldCode="DE" term="%22Boolean+algebra%22">Boolean algebra</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Abstract: New axioms for domain operations on semirings and Kleene algebras are proposed. They generalise the relational notion of domain–the set of all states that are related to some other state–to a wide range of models. They are internal since the algebras of state spaces are induced by the domain axioms. They are simpler and conceptually more appealing than previous two-sorted external approaches in which the domain algebra is determined through typing. They lead to a simple and natural algebraic approach to modal logics based on equational reasoning. The axiomatisations have been developed in a new style of computer-enhanced mathematics by automated theorem proving, and the approach itself is suitable for automated systems analysis and verification. This is demonstrated by a fully automated proof of a modal correspondence result for Löb’s formula that has applications in termination analysis. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=57369021
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.scico.2010.05.007
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 23
        StartPage: 181
    Subjects:
      – SubjectFull: Axioms
        Type: general
      – SubjectFull: Semirings (Mathematics)
        Type: general
      – SubjectFull: Kleene algebra
        Type: general
      – SubjectFull: Automatic theorem proving
        Type: general
      – SubjectFull: Distributive lattices
        Type: general
      – SubjectFull: Boolean algebra
        Type: general
    Titles:
      – TitleFull: Internal axioms for domain semirings
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Desharnais, Jules
      – PersonEntity:
          Name:
            NameFull: Struth, Georg
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 03
              Text: Mar2011
              Type: published
              Y: 2011
          Identifiers:
            – Type: issn-print
              Value: 01676423
          Numbering:
            – Type: volume
              Value: 76
            – Type: issue
              Value: 3
          Titles:
            – TitleFull: Science of Computer Programming
              Type: main
ResultId 1