An Automation-Friendly Set Theory for the B Method View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2018-05-08

AUTHORS

Guillaume Bury , Simon Cruanes , David Delahaye , Pierre-Louis Euvrard

ABSTRACT

We propose an automation-friendly set theory for the B method. This theory is expressed using first order logic extended to polymorphic types and rewriting. Rewriting is introduced along the lines of deduction modulo theory, where axioms are turned into rewrite rules over both propositions and terms. We also provide experimental results of several tools able to deal with polymorphism and rewriting over a benchmark of problems in pure set theory (i.e. without arithmetic). More... »

PAGES

409-414

References to SciGraph publications

  • 2013. TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism in AUTOMATED DEDUCTION – CADE-24
  • 2014. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations in ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z
  • 2003-09. Theorem Proving Modulo in JOURNAL OF AUTOMATED REASONING
  • Book

    TITLE

    Abstract State Machines, Alloy, B, TLA, VDM, and Z

    ISBN

    978-3-319-91270-7
    978-3-319-91271-4

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-319-91271-4_32

    DOI

    http://dx.doi.org/10.1007/978-3-319-91271-4_32

    DIMENSIONS

    https://app.dimensions.ai/details/publication/pub.1103859802


    Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
    Incoming Citations Browse incoming citations for this publication using opencitations.net

    JSON-LD is the canonical representation for SciGraph data.

    TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

    [
      {
        "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
        "about": [
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0101", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Pure Mathematics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/01", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Mathematical Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Laboratoire Sp\u00e9cification et V\u00e9rification", 
              "id": "https://www.grid.ac/institutes/grid.464035.0", 
              "name": [
                "LSV, ENS Paris-Saclay, Inria, Cachan, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Bury", 
            "givenName": "Guillaume", 
            "id": "sg:person.016210427572.93", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016210427572.93"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "name": [
                "Aesthetic Integration, Austin, TX, USA"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Cruanes", 
            "givenName": "Simon", 
            "id": "sg:person.014624007031.92", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014624007031.92"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Montpellier Laboratory of Informatics, Robotics and Microelectronics", 
              "id": "https://www.grid.ac/institutes/grid.464638.b", 
              "name": [
                "LIRMM, Universit\u00e9 de Montpellier, CNRS, Montpellier, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Delahaye", 
            "givenName": "David", 
            "id": "sg:person.014320143625.16", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014320143625.16"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Montpellier Laboratory of Informatics, Robotics and Microelectronics", 
              "id": "https://www.grid.ac/institutes/grid.464638.b", 
              "name": [
                "LIRMM, Universit\u00e9 de Montpellier, CNRS, Montpellier, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Euvrard", 
            "givenName": "Pierre-Louis", 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1023/a:1027357912519", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012883325", 
              "https://doi.org/10.1023/a:1027357912519"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-662-43652-3_26", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1013473815", 
              "https://doi.org/10.1007/978-3-662-43652-3_26"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-38574-2_29", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1031116296", 
              "https://doi.org/10.1007/978-3-642-38574-2_29"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/cbo9780511624162", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1098707935"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.29007/14v7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1100614263"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2018-05-08", 
        "datePublishedReg": "2018-05-08", 
        "description": "We propose an automation-friendly set theory for the B method. This theory is expressed using first order logic extended to polymorphic types and rewriting. Rewriting is introduced along the lines of deduction modulo theory, where axioms are turned into rewrite rules over both propositions and terms. We also provide experimental results of several tools able to deal with polymorphism and rewriting over a benchmark of problems in pure set theory (i.e. without arithmetic).", 
        "editor": [
          {
            "familyName": "Butler", 
            "givenName": "Michael", 
            "type": "Person"
          }, 
          {
            "familyName": "Raschke", 
            "givenName": "Alexander", 
            "type": "Person"
          }, 
          {
            "familyName": "Hoang", 
            "givenName": "Thai Son", 
            "type": "Person"
          }, 
          {
            "familyName": "Reichl", 
            "givenName": "Klaus", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-319-91271-4_32", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-319-91270-7", 
            "978-3-319-91271-4"
          ], 
          "name": "Abstract State Machines, Alloy, B, TLA, VDM, and Z", 
          "type": "Book"
        }, 
        "name": "An Automation-Friendly Set Theory for the B Method", 
        "pagination": "409-414", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-319-91271-4_32"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "15d89bc615fa76b1f7cd6b7f41b49c20ec8733e45f0faadad8332b18ebbc6a52"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1103859802"
            ]
          }
        ], 
        "publisher": {
          "location": "Cham", 
          "name": "Springer International Publishing", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-319-91271-4_32", 
          "https://app.dimensions.ai/details/publication/pub.1103859802"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-16T04:59", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000325_0000000325/records_100778_00000000.jsonl", 
        "type": "Chapter", 
        "url": "https://link.springer.com/10.1007%2F978-3-319-91271-4_32"
      }
    ]
     

    Download the RDF metadata as:  json-ld nt turtle xml License info

    HOW TO GET THIS DATA PROGRAMMATICALLY:

    JSON-LD is a popular format for linked data which is fully compatible with JSON.

    curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-91271-4_32'

    N-Triples is a line-based linked data format ideal for batch operations.

    curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-91271-4_32'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-91271-4_32'

    RDF/XML is a standard XML format for linked data.

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-91271-4_32'


     

    This table displays all metadata directly associated to this object as RDF triples.

    123 TRIPLES      23 PREDICATES      31 URIs      19 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-319-91271-4_32 schema:about anzsrc-for:01
    2 anzsrc-for:0101
    3 schema:author N618b017fb9aa47a9a4ff6f0889c781e2
    4 schema:citation sg:pub.10.1007/978-3-642-38574-2_29
    5 sg:pub.10.1007/978-3-662-43652-3_26
    6 sg:pub.10.1023/a:1027357912519
    7 https://doi.org/10.1017/cbo9780511624162
    8 https://doi.org/10.29007/14v7
    9 schema:datePublished 2018-05-08
    10 schema:datePublishedReg 2018-05-08
    11 schema:description We propose an automation-friendly set theory for the B method. This theory is expressed using first order logic extended to polymorphic types and rewriting. Rewriting is introduced along the lines of deduction modulo theory, where axioms are turned into rewrite rules over both propositions and terms. We also provide experimental results of several tools able to deal with polymorphism and rewriting over a benchmark of problems in pure set theory (i.e. without arithmetic).
    12 schema:editor N09a93c164729431e988badd0189973a9
    13 schema:genre chapter
    14 schema:inLanguage en
    15 schema:isAccessibleForFree false
    16 schema:isPartOf N7b19d8f29ad042c691e3bd5e432a73c3
    17 schema:name An Automation-Friendly Set Theory for the B Method
    18 schema:pagination 409-414
    19 schema:productId N019e131521e1439781e9e8c2dde46c08
    20 N779feb6e624049a2a785be9c03eedb93
    21 Nbb31fa84214b4ce8ac4f41a12b4fc699
    22 schema:publisher N7e53efd3e9ed41ff9314d36b6125b881
    23 schema:sameAs https://app.dimensions.ai/details/publication/pub.1103859802
    24 https://doi.org/10.1007/978-3-319-91271-4_32
    25 schema:sdDatePublished 2019-04-16T04:59
    26 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    27 schema:sdPublisher N848d4be0f2ee447ea48a60b34b078b75
    28 schema:url https://link.springer.com/10.1007%2F978-3-319-91271-4_32
    29 sgo:license sg:explorer/license/
    30 sgo:sdDataset chapters
    31 rdf:type schema:Chapter
    32 N019e131521e1439781e9e8c2dde46c08 schema:name doi
    33 schema:value 10.1007/978-3-319-91271-4_32
    34 rdf:type schema:PropertyValue
    35 N09a93c164729431e988badd0189973a9 rdf:first Nee7a022889ed428d8b895e0e67f20cd8
    36 rdf:rest N1c6f235a6b6045cab5f0760ece724776
    37 N09bfb3f5c59348e1a8b10a7cf65a0c3a schema:name Aesthetic Integration, Austin, TX, USA
    38 rdf:type schema:Organization
    39 N1909ed35e7aa4f418fe7e5a9212fe8a0 rdf:first sg:person.014624007031.92
    40 rdf:rest Nfeacbc30560f4846b095d54cd4fc5fab
    41 N1c6f235a6b6045cab5f0760ece724776 rdf:first N24517af2bac14e58964b76f1ea3d2c22
    42 rdf:rest Na02f6852f7ff4669b7b4179bf797ddda
    43 N24517af2bac14e58964b76f1ea3d2c22 schema:familyName Raschke
    44 schema:givenName Alexander
    45 rdf:type schema:Person
    46 N332fc70341b24c30b66542c1057d7bef rdf:first N95ee2935b7194f408afa07db8980db06
    47 rdf:rest rdf:nil
    48 N375f055efbd54c2d806e928a0a7f1fe3 schema:affiliation https://www.grid.ac/institutes/grid.464638.b
    49 schema:familyName Euvrard
    50 schema:givenName Pierre-Louis
    51 rdf:type schema:Person
    52 N618b017fb9aa47a9a4ff6f0889c781e2 rdf:first sg:person.016210427572.93
    53 rdf:rest N1909ed35e7aa4f418fe7e5a9212fe8a0
    54 N6ada83516d6c438dbb50c93b339d4cad schema:familyName Hoang
    55 schema:givenName Thai Son
    56 rdf:type schema:Person
    57 N779feb6e624049a2a785be9c03eedb93 schema:name readcube_id
    58 schema:value 15d89bc615fa76b1f7cd6b7f41b49c20ec8733e45f0faadad8332b18ebbc6a52
    59 rdf:type schema:PropertyValue
    60 N7b19d8f29ad042c691e3bd5e432a73c3 schema:isbn 978-3-319-91270-7
    61 978-3-319-91271-4
    62 schema:name Abstract State Machines, Alloy, B, TLA, VDM, and Z
    63 rdf:type schema:Book
    64 N7e53efd3e9ed41ff9314d36b6125b881 schema:location Cham
    65 schema:name Springer International Publishing
    66 rdf:type schema:Organisation
    67 N848d4be0f2ee447ea48a60b34b078b75 schema:name Springer Nature - SN SciGraph project
    68 rdf:type schema:Organization
    69 N95ee2935b7194f408afa07db8980db06 schema:familyName Reichl
    70 schema:givenName Klaus
    71 rdf:type schema:Person
    72 Na02f6852f7ff4669b7b4179bf797ddda rdf:first N6ada83516d6c438dbb50c93b339d4cad
    73 rdf:rest N332fc70341b24c30b66542c1057d7bef
    74 Nbb31fa84214b4ce8ac4f41a12b4fc699 schema:name dimensions_id
    75 schema:value pub.1103859802
    76 rdf:type schema:PropertyValue
    77 Nc2dd7cfbbfd9439ea309e7731d61234e rdf:first N375f055efbd54c2d806e928a0a7f1fe3
    78 rdf:rest rdf:nil
    79 Nee7a022889ed428d8b895e0e67f20cd8 schema:familyName Butler
    80 schema:givenName Michael
    81 rdf:type schema:Person
    82 Nfeacbc30560f4846b095d54cd4fc5fab rdf:first sg:person.014320143625.16
    83 rdf:rest Nc2dd7cfbbfd9439ea309e7731d61234e
    84 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
    85 schema:name Mathematical Sciences
    86 rdf:type schema:DefinedTerm
    87 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
    88 schema:name Pure Mathematics
    89 rdf:type schema:DefinedTerm
    90 sg:person.014320143625.16 schema:affiliation https://www.grid.ac/institutes/grid.464638.b
    91 schema:familyName Delahaye
    92 schema:givenName David
    93 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014320143625.16
    94 rdf:type schema:Person
    95 sg:person.014624007031.92 schema:affiliation N09bfb3f5c59348e1a8b10a7cf65a0c3a
    96 schema:familyName Cruanes
    97 schema:givenName Simon
    98 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014624007031.92
    99 rdf:type schema:Person
    100 sg:person.016210427572.93 schema:affiliation https://www.grid.ac/institutes/grid.464035.0
    101 schema:familyName Bury
    102 schema:givenName Guillaume
    103 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016210427572.93
    104 rdf:type schema:Person
    105 sg:pub.10.1007/978-3-642-38574-2_29 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031116296
    106 https://doi.org/10.1007/978-3-642-38574-2_29
    107 rdf:type schema:CreativeWork
    108 sg:pub.10.1007/978-3-662-43652-3_26 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013473815
    109 https://doi.org/10.1007/978-3-662-43652-3_26
    110 rdf:type schema:CreativeWork
    111 sg:pub.10.1023/a:1027357912519 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012883325
    112 https://doi.org/10.1023/a:1027357912519
    113 rdf:type schema:CreativeWork
    114 https://doi.org/10.1017/cbo9780511624162 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098707935
    115 rdf:type schema:CreativeWork
    116 https://doi.org/10.29007/14v7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1100614263
    117 rdf:type schema:CreativeWork
    118 https://www.grid.ac/institutes/grid.464035.0 schema:alternateName Laboratoire Spécification et Vérification
    119 schema:name LSV, ENS Paris-Saclay, Inria, Cachan, France
    120 rdf:type schema:Organization
    121 https://www.grid.ac/institutes/grid.464638.b schema:alternateName Montpellier Laboratory of Informatics, Robotics and Microelectronics
    122 schema:name LIRMM, Université de Montpellier, CNRS, Montpellier, France
    123 rdf:type schema:Organization
     




    Preview window. Press ESC to close (or click here)


    ...