&: 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", 
    "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", 
      "underlying logic", 
      "rules", 
      "instantiation", 
      "heuristics", 
      "sequents", 
      "terms", 
      "proof", 
      "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-08-04T17:16", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220804/entities/gbq_results/chapter/chapter_216.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.

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




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


...