Missing Proofs Found View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2001-08

AUTHORS

Branden Fitelson, Larry Wos

ABSTRACT

For close to a century, despite the efforts of fine minds that include Hilbert and Ackermann, Tarski and Bernays, Łukasiewicz, and Rose and Rosser, various proofs of a number of significant theorems have remained missing – at least not reported in the literature – amply demonstrating the depth of the corresponding problems. The types of such missing proofs are indeed diverse. For one example, a result may be guaranteed provable because of being valid, and yet no proof has been found. For a second example, a theorem may have been proved via metaargument, but the desired axiomatic proof based solely on the use of a given inference rule may have eluded the experts. For a third example, a theorem may have been announced by a master, but no proof was supplied. The finding of missing proofs of the cited types, as well as of other types, is the focus of this article. The means to finding such proofs rests with heavy use of McCune's automated reasoning program OTTER, reliance on a variety of powerful strategies this program offers, and employment of diverse methodologies. Here we present some of our successes and, because it may prove useful for circuit design and program synthesis as well as in the context of mathematics and logic, detail our approach to finding missing proofs. Well-defined and unmet challenges are included. More... »

PAGES

201-225

References to SciGraph publications

  • 1997-12. Solution of the Robbins Problem in JOURNAL OF AUTOMATED REASONING
  • 2000. Ivy: A Preprocessor and Proof Checker for First-Order Logic in COMPUTER-AIDED REASONING
  • 1996-10. OTTER and the Moufang identity problem in JOURNAL OF AUTOMATED REASONING
  • 1999-01. The Hot List Strategy in JOURNAL OF AUTOMATED REASONING
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1023/a:1010695827789

    DOI

    http://dx.doi.org/10.1023/a:1010695827789

    DIMENSIONS

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


    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/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }, 
          {
            "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"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Argonne National Laboratory", 
              "id": "https://www.grid.ac/institutes/grid.187073.a", 
              "name": [
                "Department of Philosophy, University of Wisconsin, 53706, Madison, WI, U.S.A.", 
                "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4801, Argonne, IL, U.S.A."
              ], 
              "type": "Organization"
            }, 
            "familyName": "Fitelson", 
            "givenName": "Branden", 
            "id": "sg:person.016323325740.30", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323325740.30"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Argonne National Laboratory", 
              "id": "https://www.grid.ac/institutes/grid.187073.a", 
              "name": [
                "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4801, Argonne, IL, U.S.A."
              ], 
              "type": "Organization"
            }, 
            "familyName": "Wos", 
            "givenName": "Larry", 
            "id": "sg:person.014212155341.71", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014212155341.71"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1016/0898-1221(94)00220-f", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012294032"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1090/s0002-9947-1958-0094299-1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1014994754"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/321296.321302", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1020763816"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1023/a:1005843212881", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1025423930", 
              "https://doi.org/10.1023/a:1005843212881"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00244497", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030070171", 
              "https://doi.org/10.1007/bf00244497"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00244497", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030070171", 
              "https://doi.org/10.1007/bf00244497"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-1-4757-3188-0_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1032707218", 
              "https://doi.org/10.1007/978-1-4757-3188-0_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1023/a:1005909914693", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1033518481", 
              "https://doi.org/10.1023/a:1005909914693"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/321420.321429", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1033943957"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1090/s0002-9947-1958-0094300-5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1035865209"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1305/ndjfl/1093957574", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1064916090"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2001-08", 
        "datePublishedReg": "2001-08-01", 
        "description": "For close to a century, despite the efforts of fine minds that include Hilbert and Ackermann, Tarski and Bernays, \u0141ukasiewicz, and Rose and Rosser, various proofs of a number of significant theorems have remained missing \u2013 at least not reported in the literature \u2013 amply demonstrating the depth of the corresponding problems. The types of such missing proofs are indeed diverse. For one example, a result may be guaranteed provable because of being valid, and yet no proof has been found. For a second example, a theorem may have been proved via metaargument, but the desired axiomatic proof based solely on the use of a given inference rule may have eluded the experts. For a third example, a theorem may have been announced by a master, but no proof was supplied. The finding of missing proofs of the cited types, as well as of other types, is the focus of this article. The means to finding such proofs rests with heavy use of McCune's automated reasoning program OTTER, reliance on a variety of powerful strategies this program offers, and employment of diverse methodologies. Here we present some of our successes and, because it may prove useful for circuit design and program synthesis as well as in the context of mathematics and logic, detail our approach to finding missing proofs. Well-defined and unmet challenges are included.", 
        "genre": "research_article", 
        "id": "sg:pub.10.1023/a:1010695827789", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1136522", 
            "issn": [
              "0168-7433", 
              "1573-0670"
            ], 
            "name": "Journal of Automated Reasoning", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "27"
          }
        ], 
        "name": "Missing Proofs Found", 
        "pagination": "201-225", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "40f45e666a49d375cdd634941fe4e9b278b224822843f2ba4b8ebd7d9b863cb3"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1023/a:1010695827789"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1013635039"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1023/a:1010695827789", 
          "https://app.dimensions.ai/details/publication/pub.1013635039"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-11T01:57", 
        "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/0000000001_0000000264/records_8700_00000499.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "http://link.springer.com/10.1023/A:1010695827789"
      }
    ]
     

    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.1023/a:1010695827789'

    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.1023/a:1010695827789'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1023/a:1010695827789'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1023/a:1010695827789'


     

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

    103 TRIPLES      21 PREDICATES      37 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1023/a:1010695827789 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Nffd04c2961954834a1235e750f331922
    4 schema:citation sg:pub.10.1007/978-1-4757-3188-0_16
    5 sg:pub.10.1007/bf00244497
    6 sg:pub.10.1023/a:1005843212881
    7 sg:pub.10.1023/a:1005909914693
    8 https://doi.org/10.1016/0898-1221(94)00220-f
    9 https://doi.org/10.1090/s0002-9947-1958-0094299-1
    10 https://doi.org/10.1090/s0002-9947-1958-0094300-5
    11 https://doi.org/10.1145/321296.321302
    12 https://doi.org/10.1145/321420.321429
    13 https://doi.org/10.1305/ndjfl/1093957574
    14 schema:datePublished 2001-08
    15 schema:datePublishedReg 2001-08-01
    16 schema:description For close to a century, despite the efforts of fine minds that include Hilbert and Ackermann, Tarski and Bernays, Łukasiewicz, and Rose and Rosser, various proofs of a number of significant theorems have remained missing – at least not reported in the literature – amply demonstrating the depth of the corresponding problems. The types of such missing proofs are indeed diverse. For one example, a result may be guaranteed provable because of being valid, and yet no proof has been found. For a second example, a theorem may have been proved via metaargument, but the desired axiomatic proof based solely on the use of a given inference rule may have eluded the experts. For a third example, a theorem may have been announced by a master, but no proof was supplied. The finding of missing proofs of the cited types, as well as of other types, is the focus of this article. The means to finding such proofs rests with heavy use of McCune's automated reasoning program OTTER, reliance on a variety of powerful strategies this program offers, and employment of diverse methodologies. Here we present some of our successes and, because it may prove useful for circuit design and program synthesis as well as in the context of mathematics and logic, detail our approach to finding missing proofs. Well-defined and unmet challenges are included.
    17 schema:genre research_article
    18 schema:inLanguage en
    19 schema:isAccessibleForFree false
    20 schema:isPartOf Nc3028db0b4634d6dba7d84fe0db02f4b
    21 Nce057789e6174a67bf48116009d0015e
    22 sg:journal.1136522
    23 schema:name Missing Proofs Found
    24 schema:pagination 201-225
    25 schema:productId N18ad2f3ebd0d48d4b29fe71fde4c2e05
    26 Nb9e5523141cb4b95a40d91a492023b12
    27 Nc23dc0852fcf4062827d7132103ab7f1
    28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013635039
    29 https://doi.org/10.1023/a:1010695827789
    30 schema:sdDatePublished 2019-04-11T01:57
    31 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    32 schema:sdPublisher N31c7437709b948e881b7026bbf5de757
    33 schema:url http://link.springer.com/10.1023/A:1010695827789
    34 sgo:license sg:explorer/license/
    35 sgo:sdDataset articles
    36 rdf:type schema:ScholarlyArticle
    37 N18ad2f3ebd0d48d4b29fe71fde4c2e05 schema:name dimensions_id
    38 schema:value pub.1013635039
    39 rdf:type schema:PropertyValue
    40 N31c7437709b948e881b7026bbf5de757 schema:name Springer Nature - SN SciGraph project
    41 rdf:type schema:Organization
    42 N6c7dc76ab8f147cc8905f3912522599a rdf:first sg:person.014212155341.71
    43 rdf:rest rdf:nil
    44 Nb9e5523141cb4b95a40d91a492023b12 schema:name readcube_id
    45 schema:value 40f45e666a49d375cdd634941fe4e9b278b224822843f2ba4b8ebd7d9b863cb3
    46 rdf:type schema:PropertyValue
    47 Nc23dc0852fcf4062827d7132103ab7f1 schema:name doi
    48 schema:value 10.1023/a:1010695827789
    49 rdf:type schema:PropertyValue
    50 Nc3028db0b4634d6dba7d84fe0db02f4b schema:volumeNumber 27
    51 rdf:type schema:PublicationVolume
    52 Nce057789e6174a67bf48116009d0015e schema:issueNumber 2
    53 rdf:type schema:PublicationIssue
    54 Nffd04c2961954834a1235e750f331922 rdf:first sg:person.016323325740.30
    55 rdf:rest N6c7dc76ab8f147cc8905f3912522599a
    56 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    57 schema:name Information and Computing Sciences
    58 rdf:type schema:DefinedTerm
    59 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    60 schema:name Computation Theory and Mathematics
    61 rdf:type schema:DefinedTerm
    62 sg:journal.1136522 schema:issn 0168-7433
    63 1573-0670
    64 schema:name Journal of Automated Reasoning
    65 rdf:type schema:Periodical
    66 sg:person.014212155341.71 schema:affiliation https://www.grid.ac/institutes/grid.187073.a
    67 schema:familyName Wos
    68 schema:givenName Larry
    69 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014212155341.71
    70 rdf:type schema:Person
    71 sg:person.016323325740.30 schema:affiliation https://www.grid.ac/institutes/grid.187073.a
    72 schema:familyName Fitelson
    73 schema:givenName Branden
    74 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323325740.30
    75 rdf:type schema:Person
    76 sg:pub.10.1007/978-1-4757-3188-0_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1032707218
    77 https://doi.org/10.1007/978-1-4757-3188-0_16
    78 rdf:type schema:CreativeWork
    79 sg:pub.10.1007/bf00244497 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030070171
    80 https://doi.org/10.1007/bf00244497
    81 rdf:type schema:CreativeWork
    82 sg:pub.10.1023/a:1005843212881 schema:sameAs https://app.dimensions.ai/details/publication/pub.1025423930
    83 https://doi.org/10.1023/a:1005843212881
    84 rdf:type schema:CreativeWork
    85 sg:pub.10.1023/a:1005909914693 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033518481
    86 https://doi.org/10.1023/a:1005909914693
    87 rdf:type schema:CreativeWork
    88 https://doi.org/10.1016/0898-1221(94)00220-f schema:sameAs https://app.dimensions.ai/details/publication/pub.1012294032
    89 rdf:type schema:CreativeWork
    90 https://doi.org/10.1090/s0002-9947-1958-0094299-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1014994754
    91 rdf:type schema:CreativeWork
    92 https://doi.org/10.1090/s0002-9947-1958-0094300-5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1035865209
    93 rdf:type schema:CreativeWork
    94 https://doi.org/10.1145/321296.321302 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020763816
    95 rdf:type schema:CreativeWork
    96 https://doi.org/10.1145/321420.321429 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033943957
    97 rdf:type schema:CreativeWork
    98 https://doi.org/10.1305/ndjfl/1093957574 schema:sameAs https://app.dimensions.ai/details/publication/pub.1064916090
    99 rdf:type schema:CreativeWork
    100 https://www.grid.ac/institutes/grid.187073.a schema:alternateName Argonne National Laboratory
    101 schema:name Department of Philosophy, University of Wisconsin, 53706, Madison, WI, U.S.A.
    102 Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4801, Argonne, IL, U.S.A.
    103 rdf:type schema:Organization
     




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


    ...