&: Automated natural deduction View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

1992

AUTHORS

Dave Barker-Plummer , Sidney C. Bailin , Andrew S. Merrill

ABSTRACT

In 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... »

PAGES

716-720

Book

TITLE

Automated Deduction—CADE-11

ISBN

978-3-540-55602-2
978-3-540-47252-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/3-540-55602-8_210

DOI

http://dx.doi.org/10.1007/3-540-55602-8_210

DIMENSIONS

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


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/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

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/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

Subject Predicate Object
1 sg:pub.10.1007/3-540-55602-8_210 schema:about anzsrc-for:09
2 anzsrc-for:0906
3 schema:author N947c06e6133e4425bc92a3ddd0265109
4 schema:datePublished 1992
5 schema:datePublishedReg 1992-01-01
6 schema:description In 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.
7 schema:editor N78e27ed77268410985c2cfa99e7f1403
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Nc2d57199e35e4fa6b77013c258f481a9
12 schema:keywords Zermelo set theory
13 ability
14 abstraction terms
15 addition
16 choice
17 course
18 deduction
19 formula
20 heuristics
21 inference rules
22 instantiation
23 logic
24 natural deduction
25 paper
26 proof
27 rules
28 sequents
29 set theory
30 such terms
31 system
32 terms
33 theorem
34 theory
35 underlying logic
36 usual rules
37 schema:name &: Automated natural deduction
38 schema:pagination 716-720
39 schema:productId N77b6368212674c78a9d9b95716771c5c
40 N917889a259e5483bbae8f0d0d802ea8f
41 schema:publisher Na5ce1920cfb343ee9be82793ed12c85d
42 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005028390
43 https://doi.org/10.1007/3-540-55602-8_210
44 schema:sdDatePublished 2022-06-01T22:28
45 schema:sdLicense https://scigraph.springernature.com/explorer/license/
46 schema:sdPublisher N34f2b43b3f2a46d7881d036f139ab903
47 schema:url https://doi.org/10.1007/3-540-55602-8_210
48 sgo:license sg:explorer/license/
49 sgo:sdDataset chapters
50 rdf:type schema:Chapter
51 N34f2b43b3f2a46d7881d036f139ab903 schema:name Springer Nature - SN SciGraph project
52 rdf:type schema:Organization
53 N45ea32d02ccd4089a0a99c822b890ac4 rdf:first Ne2c8d0db53dc4a048b07418b25535372
54 rdf:rest rdf:nil
55 N5e444caff4354714bc9086f089341cf9 rdf:first sg:person.011667755735.32
56 rdf:rest N45ea32d02ccd4089a0a99c822b890ac4
57 N77b6368212674c78a9d9b95716771c5c schema:name doi
58 schema:value 10.1007/3-540-55602-8_210
59 rdf:type schema:PropertyValue
60 N78e27ed77268410985c2cfa99e7f1403 rdf:first Nf9562121457547feb4080fcfdf414aba
61 rdf:rest rdf:nil
62 N917889a259e5483bbae8f0d0d802ea8f schema:name dimensions_id
63 schema:value pub.1005028390
64 rdf:type schema:PropertyValue
65 N947c06e6133e4425bc92a3ddd0265109 rdf:first sg:person.013205411157.02
66 rdf:rest N5e444caff4354714bc9086f089341cf9
67 Na5ce1920cfb343ee9be82793ed12c85d schema:name Springer Nature
68 rdf:type schema:Organisation
69 Nc2d57199e35e4fa6b77013c258f481a9 schema:isbn 978-3-540-47252-0
70 978-3-540-55602-2
71 schema:name Automated Deduction—CADE-11
72 rdf:type schema:Book
73 Ne2c8d0db53dc4a048b07418b25535372 schema:affiliation grid-institutes:grid.264430.7
74 schema:familyName Merrill
75 schema:givenName Andrew S.
76 rdf:type schema:Person
77 Nf9562121457547feb4080fcfdf414aba schema:familyName Kapur
78 schema:givenName Deepak
79 rdf:type schema:Person
80 anzsrc-for:09 schema:inDefinedTermSet anzsrc-for:
81 schema:name Engineering
82 rdf:type schema:DefinedTerm
83 anzsrc-for:0906 schema:inDefinedTermSet anzsrc-for:
84 schema:name Electrical and Electronic Engineering
85 rdf:type schema:DefinedTerm
86 sg:person.011667755735.32 schema:affiliation grid-institutes:grid.433150.0
87 schema:familyName Bailin
88 schema:givenName Sidney C.
89 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011667755735.32
90 rdf:type schema:Person
91 sg:person.013205411157.02 schema:affiliation grid-institutes:grid.264430.7
92 schema:familyName Barker-Plummer
93 schema:givenName Dave
94 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013205411157.02
95 rdf:type schema:Person
96 grid-institutes:grid.264430.7 schema:alternateName Swarthmore, College, 19081, Swarthmore, PA
97 schema:name Swarthmore, College, 19081, Swarthmore, PA
98 rdf:type schema:Organization
99 grid-institutes:grid.433150.0 schema:alternateName CTA, INCORPORATED, 6116 Executive Blvd, 20852, Rockville, Maryland
100 schema:name CTA, INCORPORATED, 6116 Executive Blvd, 20852, Rockville, Maryland
101 rdf:type schema:Organization
 




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


...