−-match: An inference rule for incrementally elaborating set instantiations View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1993-10

AUTHORS

Sidney C. Bailin, Dave Barker-Plummer

ABSTRACT

In this paper we describe a new inference rule, called −-match, which is used for finding set instantiations within an automated reasoning program. We have implemented −-match within a theorem prover called & and have used the system to prove some non-trivial theorems in mathematics, including Cantor's theorem and the correctness of transfinite induction. While not complete, we believe that −-match is a generally useful inference rule for finding set instantiations. One of the major contributions of the −-match rule is the ability to instantiate a term as an incompletely specified set abstraction, and then subsequently elaborate the identity of this set by considering other subgoals in the proof. This elaboration happens as a consequence of the deduction rules of the prover, and requires no additional machinery in the prover. More... »

PAGES

391-428

References to SciGraph publications

  • 1992. &: Automated natural deduction in AUTOMATED DEDUCTION—CADE-11
  • 1989-03. The problem of finding an inference rule for set theory in JOURNAL OF AUTOMATED REASONING
  • 1988-09. A λ-unifiability test for set theory in JOURNAL OF AUTOMATED REASONING
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/bf00881874

    DOI

    http://dx.doi.org/10.1007/bf00881874

    DIMENSIONS

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


    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/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "CTA Incorporated, 6116 Executive Blvd., Suite 800, 20852, Rockville, Maryland, USA", 
              "id": "http://www.grid.ac/institutes/grid.433150.0", 
              "name": [
                "CTA Incorporated, 6116 Executive Blvd., Suite 800, 20852, Rockville, Maryland, USA"
              ], 
              "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": "Computer Science Program, Swarthmore College, 19081, Swarthmore, Pennsylvania, USA", 
              "id": "http://www.grid.ac/institutes/grid.264430.7", 
              "name": [
                "Computer Science Program, Swarthmore College, 19081, Swarthmore, Pennsylvania, USA"
              ], 
              "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"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/bf00244943", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1017454428", 
              "https://doi.org/10.1007/bf00244943"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-55602-8_210", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1005028390", 
              "https://doi.org/10.1007/3-540-55602-8_210"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00245023", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1003776224", 
              "https://doi.org/10.1007/bf00245023"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1993-10", 
        "datePublishedReg": "1993-10-01", 
        "description": "In this paper we describe a new inference rule, called \u2212-match, which is used for finding set instantiations within an automated reasoning program. We have implemented \u2212-match within a theorem prover called & and have used the system to prove some non-trivial theorems in mathematics, including Cantor's theorem and the correctness of transfinite induction. While not complete, we believe that \u2212-match is a generally useful inference rule for finding set instantiations. One of the major contributions of the \u2212-match rule is the ability to instantiate a term as an incompletely specified set abstraction, and then subsequently elaborate the identity of this set by considering other subgoals in the proof. This elaboration happens as a consequence of the deduction rules of the prover, and requires no additional machinery in the prover.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/bf00881874", 
        "inLanguage": "en", 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1136522", 
            "issn": [
              "0168-7433", 
              "1573-0670"
            ], 
            "name": "Journal of Automated Reasoning", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "3", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "11"
          }
        ], 
        "keywords": [
          "inference rules", 
          "new inference rule", 
          "reasoning program", 
          "non-trivial theorems", 
          "deduction rules", 
          "instantiation", 
          "provers", 
          "match rules", 
          "additional machinery", 
          "rules", 
          "match", 
          "subgoals", 
          "correctness", 
          "major contribution", 
          "abstraction", 
          "proof", 
          "system", 
          "transfinite induction", 
          "theorem", 
          "mathematics", 
          "terms", 
          "program", 
          "ability", 
          "contribution", 
          "elaboration", 
          "identity", 
          "machinery", 
          "Cantor's theorem", 
          "consequences", 
          "induction", 
          "paper"
        ], 
        "name": "\u2212-match: An inference rule for incrementally elaborating set instantiations", 
        "pagination": "391-428", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1017049716"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/bf00881874"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/bf00881874", 
          "https://app.dimensions.ai/details/publication/pub.1017049716"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-06-01T22:00", 
        "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/article/article_258.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/bf00881874"
      }
    ]
     

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

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

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/bf00881874'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/bf00881874'


     

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

    111 TRIPLES      22 PREDICATES      60 URIs      49 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/bf00881874 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Nf44d437d817c4f4ba8bd3e62e309ee42
    4 schema:citation sg:pub.10.1007/3-540-55602-8_210
    5 sg:pub.10.1007/bf00244943
    6 sg:pub.10.1007/bf00245023
    7 schema:datePublished 1993-10
    8 schema:datePublishedReg 1993-10-01
    9 schema:description In this paper we describe a new inference rule, called −-match, which is used for finding set instantiations within an automated reasoning program. We have implemented −-match within a theorem prover called & and have used the system to prove some non-trivial theorems in mathematics, including Cantor's theorem and the correctness of transfinite induction. While not complete, we believe that −-match is a generally useful inference rule for finding set instantiations. One of the major contributions of the −-match rule is the ability to instantiate a term as an incompletely specified set abstraction, and then subsequently elaborate the identity of this set by considering other subgoals in the proof. This elaboration happens as a consequence of the deduction rules of the prover, and requires no additional machinery in the prover.
    10 schema:genre article
    11 schema:inLanguage en
    12 schema:isAccessibleForFree false
    13 schema:isPartOf N2cad2a8a9ce944a4920ebb1fa580142b
    14 N85b5df5a482d4b85af4cb8cbcfd449d7
    15 sg:journal.1136522
    16 schema:keywords Cantor's theorem
    17 ability
    18 abstraction
    19 additional machinery
    20 consequences
    21 contribution
    22 correctness
    23 deduction rules
    24 elaboration
    25 identity
    26 induction
    27 inference rules
    28 instantiation
    29 machinery
    30 major contribution
    31 match
    32 match rules
    33 mathematics
    34 new inference rule
    35 non-trivial theorems
    36 paper
    37 program
    38 proof
    39 provers
    40 reasoning program
    41 rules
    42 subgoals
    43 system
    44 terms
    45 theorem
    46 transfinite induction
    47 schema:name −-match: An inference rule for incrementally elaborating set instantiations
    48 schema:pagination 391-428
    49 schema:productId N6cce091c3aa049ee84cddc6e1d3ad2e5
    50 Nfa203b3ca26f46cebab933d9ff79a96c
    51 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017049716
    52 https://doi.org/10.1007/bf00881874
    53 schema:sdDatePublished 2022-06-01T22:00
    54 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    55 schema:sdPublisher Nbb5c557f824e439ba9fec0b18eaf60dd
    56 schema:url https://doi.org/10.1007/bf00881874
    57 sgo:license sg:explorer/license/
    58 sgo:sdDataset articles
    59 rdf:type schema:ScholarlyArticle
    60 N2cad2a8a9ce944a4920ebb1fa580142b schema:volumeNumber 11
    61 rdf:type schema:PublicationVolume
    62 N6cce091c3aa049ee84cddc6e1d3ad2e5 schema:name doi
    63 schema:value 10.1007/bf00881874
    64 rdf:type schema:PropertyValue
    65 N72691cbf1907479db933152b49636644 rdf:first sg:person.013205411157.02
    66 rdf:rest rdf:nil
    67 N85b5df5a482d4b85af4cb8cbcfd449d7 schema:issueNumber 3
    68 rdf:type schema:PublicationIssue
    69 Nbb5c557f824e439ba9fec0b18eaf60dd schema:name Springer Nature - SN SciGraph project
    70 rdf:type schema:Organization
    71 Nf44d437d817c4f4ba8bd3e62e309ee42 rdf:first sg:person.011667755735.32
    72 rdf:rest N72691cbf1907479db933152b49636644
    73 Nfa203b3ca26f46cebab933d9ff79a96c schema:name dimensions_id
    74 schema:value pub.1017049716
    75 rdf:type schema:PropertyValue
    76 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    77 schema:name Information and Computing Sciences
    78 rdf:type schema:DefinedTerm
    79 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    80 schema:name Computation Theory and Mathematics
    81 rdf:type schema:DefinedTerm
    82 sg:journal.1136522 schema:issn 0168-7433
    83 1573-0670
    84 schema:name Journal of Automated Reasoning
    85 schema:publisher Springer Nature
    86 rdf:type schema:Periodical
    87 sg:person.011667755735.32 schema:affiliation grid-institutes:grid.433150.0
    88 schema:familyName Bailin
    89 schema:givenName Sidney C.
    90 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011667755735.32
    91 rdf:type schema:Person
    92 sg:person.013205411157.02 schema:affiliation grid-institutes:grid.264430.7
    93 schema:familyName Barker-Plummer
    94 schema:givenName Dave
    95 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013205411157.02
    96 rdf:type schema:Person
    97 sg:pub.10.1007/3-540-55602-8_210 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005028390
    98 https://doi.org/10.1007/3-540-55602-8_210
    99 rdf:type schema:CreativeWork
    100 sg:pub.10.1007/bf00244943 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017454428
    101 https://doi.org/10.1007/bf00244943
    102 rdf:type schema:CreativeWork
    103 sg:pub.10.1007/bf00245023 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003776224
    104 https://doi.org/10.1007/bf00245023
    105 rdf:type schema:CreativeWork
    106 grid-institutes:grid.264430.7 schema:alternateName Computer Science Program, Swarthmore College, 19081, Swarthmore, Pennsylvania, USA
    107 schema:name Computer Science Program, Swarthmore College, 19081, Swarthmore, Pennsylvania, USA
    108 rdf:type schema:Organization
    109 grid-institutes:grid.433150.0 schema:alternateName CTA Incorporated, 6116 Executive Blvd., Suite 800, 20852, Rockville, Maryland, USA
    110 schema:name CTA Incorporated, 6116 Executive Blvd., Suite 800, 20852, Rockville, Maryland, USA
    111 rdf:type schema:Organization
     




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


    ...