Automating the Search for Elegant Proofs View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1998-10

AUTHORS

Larry Wos

ABSTRACT

The research reported in this article was spawned by a colleague's request to find an elegant proof (of a theorem from Boolean algebra) to replace his proof consisting of 816 deduced steps. The request was met by finding a proof consisting of 100 deduced steps. The methodology used to obtain the far shorter proof is presented in detail through a sequence of experiments. Although clearly not an algorithm, the methodology is sufficiently general to enable its use for seeking elegant proofs regardless of the domain of study. In addition to (usually) being more elegant, shorter proofs often provide the needed path to constructing a more efficient circuit, a more effective algorithm, and the like. The methodology relies heavily on the assistance of McCune's automated reasoning program OTTER. Of the aspects of proof elegance, the main focus here is on proof length, with brief attention paid to the type of term present, the number of variables required, and the complexity of deduced steps. The methodology is iterative, relying heavily on the use of three strategies: the resonance strategy, the hot list strategy, and McCune's ratio strategy. These strategies, as well as other features on which the methodology relies, do exhibit tendencies that can be exploited in the search for shorter proofs and for other objectives. To provide some insight regarding the value of the methodology, I discuss its successful application to other problems from Boolean algebra and to problems from lattice theory. Research suggestions and challenges are also offered. More... »

PAGES

135-175

References to SciGraph publications

  • 1996-10. OTTER and the Moufang identity problem in JOURNAL OF AUTOMATED REASONING
  • 1983-12. Condensed detachment as a rule of inference in STUDIA LOGICA
  • 1992. Basic paramodulation and superposition in AUTOMATED DEDUCTION—CADE-11
  • 1991. Automated Reasoning and Bledsoe’s Dream for the Field in AUTOMATED REASONING
  • 1996-06. Using hints to increase the effectiveness of an automated reasoning program: Case studies in JOURNAL OF AUTOMATED REASONING
  • 1992-06. The application of automated reasoning to questions in mathematics and logic in ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
  • 1996-08. The power of combining resonance with heat in JOURNAL OF AUTOMATED REASONING
  • 1995-10. Searching for circles of pure proofs in JOURNAL OF AUTOMATED REASONING
  • Identifiers

    URI

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

    DOI

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

    DIMENSIONS

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


    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": [
                "Argonne National Laboratory, Mathematics and Computer Science Division, Argonne, Illinois, 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": "sg:pub.10.1007/bf00881802", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1001072401", 
              "https://doi.org/10.1007/bf00881802"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01371632", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004366401", 
              "https://doi.org/10.1007/bf01371632"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01371632", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004366401", 
              "https://doi.org/10.1007/bf01371632"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00247668", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004671454", 
              "https://doi.org/10.1007/bf00247668"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00247668", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004671454", 
              "https://doi.org/10.1007/bf00247668"
            ], 
            "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.1016/0898-1221(94)00220-f", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012294032"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-55602-8_185", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022595714", 
              "https://doi.org/10.1007/3-540-55602-8_185"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01543481", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1023969650", 
              "https://doi.org/10.1007/bf01543481"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01543481", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1023969650", 
              "https://doi.org/10.1007/bf01543481"
            ], 
            "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": "https://doi.org/10.1090/s0002-9939-1973-0325498-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049992353"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1305/ndjfl/1093888216", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1064915366"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1998-10", 
        "datePublishedReg": "1998-10-01", 
        "description": "The research reported in this article was spawned by a colleague's request to find an elegant proof (of a theorem from Boolean algebra) to replace his proof consisting of 816 deduced steps. The request was met by finding a proof consisting of 100 deduced steps. The methodology used to obtain the far shorter proof is presented in detail through a sequence of experiments. Although clearly not an algorithm, the methodology is sufficiently general to enable its use for seeking elegant proofs regardless of the domain of study. In addition to (usually) being more elegant, shorter proofs often provide the needed path to constructing a more efficient circuit, a more effective algorithm, and the like. The methodology relies heavily on the assistance of McCune's automated reasoning program OTTER. Of the aspects of proof elegance, the main focus here is on proof length, with brief attention paid to the type of term present, the number of variables required, and the complexity of deduced steps. The methodology is iterative, relying heavily on the use of three strategies: the resonance strategy, the hot list strategy, and McCune's ratio strategy. These strategies, as well as other features on which the methodology relies, do exhibit tendencies that can be exploited in the search for shorter proofs and for other objectives. To provide some insight regarding the value of the methodology, I discuss its successful application to other problems from Boolean algebra and to problems from lattice theory. Research suggestions and challenges are also offered.", 
        "genre": "research_article", 
        "id": "sg:pub.10.1023/a:1005847113370", 
        "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": "21"
          }
        ], 
        "name": "Automating the Search for Elegant Proofs", 
        "pagination": "135-175", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "b03df2da9ab67c52fbbdbfd15d6a0effb3889f7b6d9d2425c1f3eaa7679e5375"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1023/a:1005847113370"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1036997145"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1023/a:1005847113370", 
          "https://app.dimensions.ai/details/publication/pub.1036997145"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-10T18:18", 
        "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_8675_00000500.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "http://link.springer.com/10.1023/A:1005847113370"
      }
    ]
     

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

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

    Turtle is a human-readable linked data format.

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

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

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


     

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

    102 TRIPLES      21 PREDICATES      38 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1023/a:1005847113370 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author N6bbbfba382b4411cae7970b7111c42ff
    4 schema:citation sg:pub.10.1007/3-540-55602-8_185
    5 sg:pub.10.1007/978-94-011-3488-0_15
    6 sg:pub.10.1007/bf00244497
    7 sg:pub.10.1007/bf00247668
    8 sg:pub.10.1007/bf00252178
    9 sg:pub.10.1007/bf00881802
    10 sg:pub.10.1007/bf01371632
    11 sg:pub.10.1007/bf01543481
    12 https://doi.org/10.1016/0898-1221(94)00220-f
    13 https://doi.org/10.1090/s0002-9939-1973-0325498-2
    14 https://doi.org/10.1305/ndjfl/1093888216
    15 schema:datePublished 1998-10
    16 schema:datePublishedReg 1998-10-01
    17 schema:description The research reported in this article was spawned by a colleague's request to find an elegant proof (of a theorem from Boolean algebra) to replace his proof consisting of 816 deduced steps. The request was met by finding a proof consisting of 100 deduced steps. The methodology used to obtain the far shorter proof is presented in detail through a sequence of experiments. Although clearly not an algorithm, the methodology is sufficiently general to enable its use for seeking elegant proofs regardless of the domain of study. In addition to (usually) being more elegant, shorter proofs often provide the needed path to constructing a more efficient circuit, a more effective algorithm, and the like. The methodology relies heavily on the assistance of McCune's automated reasoning program OTTER. Of the aspects of proof elegance, the main focus here is on proof length, with brief attention paid to the type of term present, the number of variables required, and the complexity of deduced steps. The methodology is iterative, relying heavily on the use of three strategies: the resonance strategy, the hot list strategy, and McCune's ratio strategy. These strategies, as well as other features on which the methodology relies, do exhibit tendencies that can be exploited in the search for shorter proofs and for other objectives. To provide some insight regarding the value of the methodology, I discuss its successful application to other problems from Boolean algebra and to problems from lattice theory. Research suggestions and challenges are also offered.
    18 schema:genre research_article
    19 schema:inLanguage en
    20 schema:isAccessibleForFree false
    21 schema:isPartOf Nc9578e7e25b64ec7bdda5d79a67b1e0d
    22 Ndc2d1922f70840298466ec184b32b921
    23 sg:journal.1136522
    24 schema:name Automating the Search for Elegant Proofs
    25 schema:pagination 135-175
    26 schema:productId N3c9782d72d9d4f528dc14217f30d4f02
    27 N421325b1adc2418c81f4a9d9ae116ebd
    28 Nc846db399abb4114900e432cbdab3ffe
    29 schema:sameAs https://app.dimensions.ai/details/publication/pub.1036997145
    30 https://doi.org/10.1023/a:1005847113370
    31 schema:sdDatePublished 2019-04-10T18:18
    32 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    33 schema:sdPublisher N2e911c69c4a646ad8eee0ee5402f7c51
    34 schema:url http://link.springer.com/10.1023/A:1005847113370
    35 sgo:license sg:explorer/license/
    36 sgo:sdDataset articles
    37 rdf:type schema:ScholarlyArticle
    38 N2e911c69c4a646ad8eee0ee5402f7c51 schema:name Springer Nature - SN SciGraph project
    39 rdf:type schema:Organization
    40 N3c9782d72d9d4f528dc14217f30d4f02 schema:name readcube_id
    41 schema:value b03df2da9ab67c52fbbdbfd15d6a0effb3889f7b6d9d2425c1f3eaa7679e5375
    42 rdf:type schema:PropertyValue
    43 N421325b1adc2418c81f4a9d9ae116ebd schema:name dimensions_id
    44 schema:value pub.1036997145
    45 rdf:type schema:PropertyValue
    46 N6bbbfba382b4411cae7970b7111c42ff rdf:first sg:person.014212155341.71
    47 rdf:rest rdf:nil
    48 Nc846db399abb4114900e432cbdab3ffe schema:name doi
    49 schema:value 10.1023/a:1005847113370
    50 rdf:type schema:PropertyValue
    51 Nc9578e7e25b64ec7bdda5d79a67b1e0d schema:volumeNumber 21
    52 rdf:type schema:PublicationVolume
    53 Ndc2d1922f70840298466ec184b32b921 schema:issueNumber 2
    54 rdf:type schema:PublicationIssue
    55 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    56 schema:name Information and Computing Sciences
    57 rdf:type schema:DefinedTerm
    58 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    59 schema:name Computation Theory and Mathematics
    60 rdf:type schema:DefinedTerm
    61 sg:journal.1136522 schema:issn 0168-7433
    62 1573-0670
    63 schema:name Journal of Automated Reasoning
    64 rdf:type schema:Periodical
    65 sg:person.014212155341.71 schema:affiliation https://www.grid.ac/institutes/grid.187073.a
    66 schema:familyName Wos
    67 schema:givenName Larry
    68 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014212155341.71
    69 rdf:type schema:Person
    70 sg:pub.10.1007/3-540-55602-8_185 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022595714
    71 https://doi.org/10.1007/3-540-55602-8_185
    72 rdf:type schema:CreativeWork
    73 sg:pub.10.1007/978-94-011-3488-0_15 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008246432
    74 https://doi.org/10.1007/978-94-011-3488-0_15
    75 rdf:type schema:CreativeWork
    76 sg:pub.10.1007/bf00244497 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030070171
    77 https://doi.org/10.1007/bf00244497
    78 rdf:type schema:CreativeWork
    79 sg:pub.10.1007/bf00247668 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004671454
    80 https://doi.org/10.1007/bf00247668
    81 rdf:type schema:CreativeWork
    82 sg:pub.10.1007/bf00252178 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006042548
    83 https://doi.org/10.1007/bf00252178
    84 rdf:type schema:CreativeWork
    85 sg:pub.10.1007/bf00881802 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001072401
    86 https://doi.org/10.1007/bf00881802
    87 rdf:type schema:CreativeWork
    88 sg:pub.10.1007/bf01371632 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004366401
    89 https://doi.org/10.1007/bf01371632
    90 rdf:type schema:CreativeWork
    91 sg:pub.10.1007/bf01543481 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023969650
    92 https://doi.org/10.1007/bf01543481
    93 rdf:type schema:CreativeWork
    94 https://doi.org/10.1016/0898-1221(94)00220-f schema:sameAs https://app.dimensions.ai/details/publication/pub.1012294032
    95 rdf:type schema:CreativeWork
    96 https://doi.org/10.1090/s0002-9939-1973-0325498-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049992353
    97 rdf:type schema:CreativeWork
    98 https://doi.org/10.1305/ndjfl/1093888216 schema:sameAs https://app.dimensions.ai/details/publication/pub.1064915366
    99 rdf:type schema:CreativeWork
    100 https://www.grid.ac/institutes/grid.187073.a schema:alternateName Argonne National Laboratory
    101 schema:name Argonne National Laboratory, Mathematics and Computer Science Division, Argonne, Illinois, U.S.A
    102 rdf:type schema:Organization
     




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


    ...