Solving Open Questions and Other Challenge Problems Using Proof Sketches View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2001-08

AUTHORS

Robert Veroff

ABSTRACT

In this article, we describe a set of procedures and strategies for searching for proofs in logical systems based on the inference rule condensed detachment. The procedures and strategies rely on the derivation of proof sketches – sequences of formulas that are used as hints to guide the search for sound proofs. In the simplest case, a proof sketch consists of a subproof – key lemmas to prove, for example – and the proof is completed by filling in the missing steps. In the more general case, a proof sketch consists of a sequence of formulas sufficient to find a proof, but it may include formulas that are not provable in the current theory. We find that even in this more general case, proof sketches can provide valuable guidance in finding sound proofs. Proof sketches have been used successfully for numerous problems coming from a variety of problem areas. We have, for example, used proof sketches to find several new two-axiom systems for Boolean algebra using the Sheffer stroke. More... »

PAGES

157-174

References to SciGraph publications

  • 1988. Analogical reasoning and proof discovery in 9TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
  • 1984. The Linked Inference Principle, II: The User’s Viewpoint in 7TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
  • 1992-06. Gazing: An approach to the problem of definition and lemma use in JOURNAL OF AUTOMATED REASONING
  • 1991. Automated Reasoning and Bledsoe’s Dream for the Field in AUTOMATED REASONING
  • 1992-04. The linked inference principle, I: The formal treatment in JOURNAL OF AUTOMATED REASONING
  • 1996-06. Using hints to increase the effectiveness of an automated reasoning program: Case studies in JOURNAL OF AUTOMATED REASONING
  • 1980. Abstraction mappings in mechanical theorem proving in 5TH CONFERENCE ON AUTOMATED DEDUCTION LES ARCS, FRANCE, JULY 8–11, 1980
  • Identifiers

    URI

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

    DOI

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

    DIMENSIONS

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


    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": "University of New Mexico", 
              "id": "https://www.grid.ac/institutes/grid.266832.b", 
              "name": [
                "University of New Mexico, 87131, Albuquerque, NM, U.S.A"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Veroff", 
            "givenName": "Robert", 
            "id": "sg:person.0644424756.64", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0644424756.64"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-0-387-34768-4_19", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1005893084", 
              "https://doi.org/10.1007/978-0-387-34768-4_19"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-0-387-34768-4_19", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1005893084", 
              "https://doi.org/10.1007/978-0-387-34768-4_19"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00252178", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006042548", 
              "https://doi.org/10.1007/bf00252178"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00252178", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006042548", 
              "https://doi.org/10.1007/bf00252178"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-94-011-3488-0_15", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008246432", 
              "https://doi.org/10.1007/978-94-011-3488-0_15"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-94-011-3488-0_15", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008246432", 
              "https://doi.org/10.1007/978-94-011-3488-0_15"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1090/s0002-9947-1913-1500960-1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1009726149"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0004-3702(74)90026-5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022737316"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0004-3702(74)90026-5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022737316"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00244283", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024762168", 
              "https://doi.org/10.1007/bf00244283"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00244283", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024762168", 
              "https://doi.org/10.1007/bf00244283"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0004-3702(92)90021-o", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024841122"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0004-3702(92)90021-o", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024841122"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0012849", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1033434676", 
              "https://doi.org/10.1007/bfb0012849"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-10009-1_21", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038411807", 
              "https://doi.org/10.1007/3-540-10009-1_21"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0898-1221(76)90002-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044945425"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf02341853", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1046287944", 
              "https://doi.org/10.1007/bf02341853"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf02341853", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1046287944", 
              "https://doi.org/10.1007/bf02341853"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1305/ndjfl/1093893713", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1064915781"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2001-08", 
        "datePublishedReg": "2001-08-01", 
        "description": "In this article, we describe a set of procedures and strategies for searching for proofs in logical systems based on the inference rule condensed detachment. The procedures and strategies rely on the derivation of proof sketches \u2013 sequences of formulas that are used as hints to guide the search for sound proofs. In the simplest case, a proof sketch consists of a subproof \u2013 key lemmas to prove, for example \u2013 and the proof is completed by filling in the missing steps. In the more general case, a proof sketch consists of a sequence of formulas sufficient to find a proof, but it may include formulas that are not provable in the current theory. We find that even in this more general case, proof sketches can provide valuable guidance in finding sound proofs. Proof sketches have been used successfully for numerous problems coming from a variety of problem areas. We have, for example, used proof sketches to find several new two-axiom systems for Boolean algebra using the Sheffer stroke.", 
        "genre": "research_article", 
        "id": "sg:pub.10.1023/a:1010639725972", 
        "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": "Solving Open Questions and Other Challenge Problems Using Proof Sketches", 
        "pagination": "157-174", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "0ad979b17258341ba308a9ec3d5c37a88ed058993c5b626be4686f32806f1c71"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1023/a:1010639725972"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1002278623"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1023/a:1010639725972", 
          "https://app.dimensions.ai/details/publication/pub.1002278623"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-10T14: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_8663_00000498.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "http://link.springer.com/10.1023/A:1010639725972"
      }
    ]
     

    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:1010639725972'

    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:1010639725972'

    Turtle is a human-readable linked data format.

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

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

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


     

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

    104 TRIPLES      21 PREDICATES      39 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1023/a:1010639725972 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author N8615804d92794aaca258e5bc39d7c697
    4 schema:citation sg:pub.10.1007/3-540-10009-1_21
    5 sg:pub.10.1007/978-0-387-34768-4_19
    6 sg:pub.10.1007/978-94-011-3488-0_15
    7 sg:pub.10.1007/bf00244283
    8 sg:pub.10.1007/bf00252178
    9 sg:pub.10.1007/bf02341853
    10 sg:pub.10.1007/bfb0012849
    11 https://doi.org/10.1016/0004-3702(74)90026-5
    12 https://doi.org/10.1016/0004-3702(92)90021-o
    13 https://doi.org/10.1016/0898-1221(76)90002-x
    14 https://doi.org/10.1090/s0002-9947-1913-1500960-1
    15 https://doi.org/10.1305/ndjfl/1093893713
    16 schema:datePublished 2001-08
    17 schema:datePublishedReg 2001-08-01
    18 schema:description In this article, we describe a set of procedures and strategies for searching for proofs in logical systems based on the inference rule condensed detachment. The procedures and strategies rely on the derivation of proof sketches – sequences of formulas that are used as hints to guide the search for sound proofs. In the simplest case, a proof sketch consists of a subproof – key lemmas to prove, for example – and the proof is completed by filling in the missing steps. In the more general case, a proof sketch consists of a sequence of formulas sufficient to find a proof, but it may include formulas that are not provable in the current theory. We find that even in this more general case, proof sketches can provide valuable guidance in finding sound proofs. Proof sketches have been used successfully for numerous problems coming from a variety of problem areas. We have, for example, used proof sketches to find several new two-axiom systems for Boolean algebra using the Sheffer stroke.
    19 schema:genre research_article
    20 schema:inLanguage en
    21 schema:isAccessibleForFree false
    22 schema:isPartOf N5d1fd1be161b4424999ba16e353c2ba5
    23 N8aad8de50764418288d6d8f450813833
    24 sg:journal.1136522
    25 schema:name Solving Open Questions and Other Challenge Problems Using Proof Sketches
    26 schema:pagination 157-174
    27 schema:productId N1f3897d525cf4580a955f442e494bcfa
    28 N6275288e23cc4de88398ce7448c2b77b
    29 N8125c1edfdc34e1fab8dcb05293178ce
    30 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002278623
    31 https://doi.org/10.1023/a:1010639725972
    32 schema:sdDatePublished 2019-04-10T14:57
    33 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    34 schema:sdPublisher Nca4d2f5293ed42b796074bb07a2060bd
    35 schema:url http://link.springer.com/10.1023/A:1010639725972
    36 sgo:license sg:explorer/license/
    37 sgo:sdDataset articles
    38 rdf:type schema:ScholarlyArticle
    39 N1f3897d525cf4580a955f442e494bcfa schema:name dimensions_id
    40 schema:value pub.1002278623
    41 rdf:type schema:PropertyValue
    42 N5d1fd1be161b4424999ba16e353c2ba5 schema:volumeNumber 27
    43 rdf:type schema:PublicationVolume
    44 N6275288e23cc4de88398ce7448c2b77b schema:name readcube_id
    45 schema:value 0ad979b17258341ba308a9ec3d5c37a88ed058993c5b626be4686f32806f1c71
    46 rdf:type schema:PropertyValue
    47 N8125c1edfdc34e1fab8dcb05293178ce schema:name doi
    48 schema:value 10.1023/a:1010639725972
    49 rdf:type schema:PropertyValue
    50 N8615804d92794aaca258e5bc39d7c697 rdf:first sg:person.0644424756.64
    51 rdf:rest rdf:nil
    52 N8aad8de50764418288d6d8f450813833 schema:issueNumber 2
    53 rdf:type schema:PublicationIssue
    54 Nca4d2f5293ed42b796074bb07a2060bd schema:name Springer Nature - SN SciGraph project
    55 rdf:type schema:Organization
    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.0644424756.64 schema:affiliation https://www.grid.ac/institutes/grid.266832.b
    67 schema:familyName Veroff
    68 schema:givenName Robert
    69 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0644424756.64
    70 rdf:type schema:Person
    71 sg:pub.10.1007/3-540-10009-1_21 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038411807
    72 https://doi.org/10.1007/3-540-10009-1_21
    73 rdf:type schema:CreativeWork
    74 sg:pub.10.1007/978-0-387-34768-4_19 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005893084
    75 https://doi.org/10.1007/978-0-387-34768-4_19
    76 rdf:type schema:CreativeWork
    77 sg:pub.10.1007/978-94-011-3488-0_15 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008246432
    78 https://doi.org/10.1007/978-94-011-3488-0_15
    79 rdf:type schema:CreativeWork
    80 sg:pub.10.1007/bf00244283 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024762168
    81 https://doi.org/10.1007/bf00244283
    82 rdf:type schema:CreativeWork
    83 sg:pub.10.1007/bf00252178 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006042548
    84 https://doi.org/10.1007/bf00252178
    85 rdf:type schema:CreativeWork
    86 sg:pub.10.1007/bf02341853 schema:sameAs https://app.dimensions.ai/details/publication/pub.1046287944
    87 https://doi.org/10.1007/bf02341853
    88 rdf:type schema:CreativeWork
    89 sg:pub.10.1007/bfb0012849 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033434676
    90 https://doi.org/10.1007/bfb0012849
    91 rdf:type schema:CreativeWork
    92 https://doi.org/10.1016/0004-3702(74)90026-5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022737316
    93 rdf:type schema:CreativeWork
    94 https://doi.org/10.1016/0004-3702(92)90021-o schema:sameAs https://app.dimensions.ai/details/publication/pub.1024841122
    95 rdf:type schema:CreativeWork
    96 https://doi.org/10.1016/0898-1221(76)90002-x schema:sameAs https://app.dimensions.ai/details/publication/pub.1044945425
    97 rdf:type schema:CreativeWork
    98 https://doi.org/10.1090/s0002-9947-1913-1500960-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009726149
    99 rdf:type schema:CreativeWork
    100 https://doi.org/10.1305/ndjfl/1093893713 schema:sameAs https://app.dimensions.ai/details/publication/pub.1064915781
    101 rdf:type schema:CreativeWork
    102 https://www.grid.ac/institutes/grid.266832.b schema:alternateName University of New Mexico
    103 schema:name University of New Mexico, 87131, Albuquerque, NM, U.S.A
    104 rdf:type schema:Organization
     




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


    ...