2018-05-08
AUTHORSGuillaume Bury , Simon Cruanes , David Delahaye , Pierre-Louis Euvrard
ABSTRACTWe 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... »
PAGES409-414
Abstract State Machines, Alloy, B, TLA, VDM, and Z
ISBN
978-3-319-91270-7
978-3-319-91271-4
http://scigraph.springernature.com/pub.10.1007/978-3-319-91271-4_32
DOIhttp://dx.doi.org/10.1007/978-3-319-91271-4_32
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1103859802
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
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