1992
AUTHORSDave Barker-Plummer , Sidney C. Bailin , Andrew S. Merrill
ABSTRACTIn this paper we describe a sequent calculus-based theorem prover called −5. The underlying logic of & is that of Zermelo set theory. In addition to the usual rules of first-order sequent based systems, the logic contains inference rules to handle set abstraction terms, including the ability to unify formulae involving such terms, and the ability to introduce new abstraction terms as instantiations. & also has novel derived rules and heuristics for making choices in the course of the proof of a theorem. More... »
PAGES716-720
Automated Deduction—CADE-11
ISBN
978-3-540-55602-2
978-3-540-47252-0
http://scigraph.springernature.com/pub.10.1007/3-540-55602-8_210
DOIhttp://dx.doi.org/10.1007/3-540-55602-8_210
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1005028390
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/09",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Engineering",
"type": "DefinedTerm"
},
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0906",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Electrical and Electronic Engineering",
"type": "DefinedTerm"
}
],
"author": [
{
"affiliation": {
"alternateName": "Swarthmore, College, 19081, Swarthmore, PA",
"id": "http://www.grid.ac/institutes/grid.264430.7",
"name": [
"Swarthmore, College, 19081, Swarthmore, PA"
],
"type": "Organization"
},
"familyName": "Barker-Plummer",
"givenName": "Dave",
"id": "sg:person.013205411157.02",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013205411157.02"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "CTA, INCORPORATED, 6116 Executive Blvd, 20852, Rockville, Maryland",
"id": "http://www.grid.ac/institutes/grid.433150.0",
"name": [
"CTA, INCORPORATED, 6116 Executive Blvd, 20852, Rockville, Maryland"
],
"type": "Organization"
},
"familyName": "Bailin",
"givenName": "Sidney C.",
"id": "sg:person.011667755735.32",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011667755735.32"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Swarthmore, College, 19081, Swarthmore, PA",
"id": "http://www.grid.ac/institutes/grid.264430.7",
"name": [
"Swarthmore, College, 19081, Swarthmore, PA"
],
"type": "Organization"
},
"familyName": "Merrill",
"givenName": "Andrew S.",
"type": "Person"
}
],
"datePublished": "1992",
"datePublishedReg": "1992-01-01",
"description": "In this paper we describe a sequent calculus-based theorem prover called \u22125. The underlying logic of & is that of Zermelo set theory. In addition to the usual rules of first-order sequent based systems, the logic contains inference rules to handle set abstraction terms, including the ability to unify formulae involving such terms, and the ability to introduce new abstraction terms as instantiations. & also has novel derived rules and heuristics for making choices in the course of the proof of a theorem.",
"editor": [
{
"familyName": "Kapur",
"givenName": "Deepak",
"type": "Person"
}
],
"genre": "chapter",
"id": "sg:pub.10.1007/3-540-55602-8_210",
"inLanguage": "en",
"isAccessibleForFree": false,
"isPartOf": {
"isbn": [
"978-3-540-55602-2",
"978-3-540-47252-0"
],
"name": "Automated Deduction\u2014CADE-11",
"type": "Book"
},
"keywords": [
"inference rules",
"set theory",
"abstraction terms",
"Zermelo set theory",
"logic",
"natural deduction",
"rules",
"underlying logic",
"instantiation",
"heuristics",
"sequents",
"proof",
"terms",
"system",
"deduction",
"ability",
"theorem",
"usual rules",
"such terms",
"choice",
"theory",
"addition",
"formula",
"course",
"paper"
],
"name": "&: Automated natural deduction",
"pagination": "716-720",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1005028390"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/3-540-55602-8_210"
]
}
],
"publisher": {
"name": "Springer Nature",
"type": "Organisation"
},
"sameAs": [
"https://doi.org/10.1007/3-540-55602-8_210",
"https://app.dimensions.ai/details/publication/pub.1005028390"
],
"sdDataset": "chapters",
"sdDatePublished": "2022-06-01T22:28",
"sdLicense": "https://scigraph.springernature.com/explorer/license/",
"sdPublisher": {
"name": "Springer Nature - SN SciGraph project",
"type": "Organization"
},
"sdSource": "s3://com-springernature-scigraph/baseset/20220601/entities/gbq_results/chapter/chapter_158.jsonl",
"type": "Chapter",
"url": "https://doi.org/10.1007/3-540-55602-8_210"
}
]
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/3-540-55602-8_210'
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/3-540-55602-8_210'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-55602-8_210'
RDF/XML is a standard XML format for linked data.
curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/3-540-55602-8_210'
This table displays all metadata directly associated to this object as RDF triples.
101 TRIPLES
23 PREDICATES
51 URIs
44 LITERALS
7 BLANK NODES