Finding Shortest Proofs: An Application of Linked Inference Rules View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2001-08

AUTHORS

Robert Veroff

ABSTRACT

In this article, we describe a procedure for systematically searching for shortest proofs in logical systems based on the inference rule condensed detachment. The procedure relies on applications of linked UR-resolution and uses demodulation to categorize derivations. Although the procedure is exhaustive in nature – and therefore realistically is applicable only to relatively small problems – it is shown to overcome the obstacles to finding shortest proofs presented by ordinary resolution-style theorem proving. More... »

PAGES

123-139

References to SciGraph publications

  • 1992-04. The linked inference principle, I: The formal treatment in JOURNAL OF AUTOMATED REASONING
  • 1984. The Linked Inference Principle, II: The User’s Viewpoint in 7TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
  • Identifiers

    URI

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

    DOI

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

    DIMENSIONS

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


    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/1701", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Psychology", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/17", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Psychology and Cognitive 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/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"
          }
        ], 
        "datePublished": "2001-08", 
        "datePublishedReg": "2001-08-01", 
        "description": "In this article, we describe a procedure for systematically searching for shortest proofs in logical systems based on the inference rule condensed detachment. The procedure relies on applications of linked UR-resolution and uses demodulation to categorize derivations. Although the procedure is exhaustive in nature \u2013 and therefore realistically is applicable only to relatively small problems \u2013 it is shown to overcome the obstacles to finding shortest proofs presented by ordinary resolution-style theorem proving.", 
        "genre": "research_article", 
        "id": "sg:pub.10.1023/a:1010635625063", 
        "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": "Finding Shortest Proofs: An Application of Linked Inference Rules", 
        "pagination": "123-139", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "665629306c42863ac5eaa0ba3bf6430bd4ee2b0f7c458de1cd68c03c924898d8"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1023/a:1010635625063"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1021478966"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1023/a:1010635625063", 
          "https://app.dimensions.ai/details/publication/pub.1021478966"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-10T14:06", 
        "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_8660_00000499.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "http://link.springer.com/10.1023/A:1010635625063"
      }
    ]
     

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

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

    Turtle is a human-readable linked data format.

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

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

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


     

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

    69 TRIPLES      21 PREDICATES      29 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1023/a:1010635625063 schema:about anzsrc-for:17
    2 anzsrc-for:1701
    3 schema:author Ndc25b0d732fc47ac9c63afdd8fc3b026
    4 schema:citation sg:pub.10.1007/978-0-387-34768-4_19
    5 sg:pub.10.1007/bf00244283
    6 schema:datePublished 2001-08
    7 schema:datePublishedReg 2001-08-01
    8 schema:description In this article, we describe a procedure for systematically searching for shortest proofs in logical systems based on the inference rule condensed detachment. The procedure relies on applications of linked UR-resolution and uses demodulation to categorize derivations. Although the procedure is exhaustive in nature – and therefore realistically is applicable only to relatively small problems – it is shown to overcome the obstacles to finding shortest proofs presented by ordinary resolution-style theorem proving.
    9 schema:genre research_article
    10 schema:inLanguage en
    11 schema:isAccessibleForFree false
    12 schema:isPartOf N7490c897c04646ed99748bbd4f74d4d1
    13 Na839f214ae5d4d2082324f3224564cbd
    14 sg:journal.1136522
    15 schema:name Finding Shortest Proofs: An Application of Linked Inference Rules
    16 schema:pagination 123-139
    17 schema:productId N3a2fd35489a74f89af691e83cd3d0744
    18 Nb99f96fa680441eb8ef6486506540280
    19 Nca5805a6b5c944fb847b6904b314f0f4
    20 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021478966
    21 https://doi.org/10.1023/a:1010635625063
    22 schema:sdDatePublished 2019-04-10T14:06
    23 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    24 schema:sdPublisher N58e74f100f87436ebd8778c8b27a9809
    25 schema:url http://link.springer.com/10.1023/A:1010635625063
    26 sgo:license sg:explorer/license/
    27 sgo:sdDataset articles
    28 rdf:type schema:ScholarlyArticle
    29 N3a2fd35489a74f89af691e83cd3d0744 schema:name doi
    30 schema:value 10.1023/a:1010635625063
    31 rdf:type schema:PropertyValue
    32 N58e74f100f87436ebd8778c8b27a9809 schema:name Springer Nature - SN SciGraph project
    33 rdf:type schema:Organization
    34 N7490c897c04646ed99748bbd4f74d4d1 schema:volumeNumber 27
    35 rdf:type schema:PublicationVolume
    36 Na839f214ae5d4d2082324f3224564cbd schema:issueNumber 2
    37 rdf:type schema:PublicationIssue
    38 Nb99f96fa680441eb8ef6486506540280 schema:name dimensions_id
    39 schema:value pub.1021478966
    40 rdf:type schema:PropertyValue
    41 Nca5805a6b5c944fb847b6904b314f0f4 schema:name readcube_id
    42 schema:value 665629306c42863ac5eaa0ba3bf6430bd4ee2b0f7c458de1cd68c03c924898d8
    43 rdf:type schema:PropertyValue
    44 Ndc25b0d732fc47ac9c63afdd8fc3b026 rdf:first sg:person.0644424756.64
    45 rdf:rest rdf:nil
    46 anzsrc-for:17 schema:inDefinedTermSet anzsrc-for:
    47 schema:name Psychology and Cognitive Sciences
    48 rdf:type schema:DefinedTerm
    49 anzsrc-for:1701 schema:inDefinedTermSet anzsrc-for:
    50 schema:name Psychology
    51 rdf:type schema:DefinedTerm
    52 sg:journal.1136522 schema:issn 0168-7433
    53 1573-0670
    54 schema:name Journal of Automated Reasoning
    55 rdf:type schema:Periodical
    56 sg:person.0644424756.64 schema:affiliation https://www.grid.ac/institutes/grid.266832.b
    57 schema:familyName Veroff
    58 schema:givenName Robert
    59 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0644424756.64
    60 rdf:type schema:Person
    61 sg:pub.10.1007/978-0-387-34768-4_19 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005893084
    62 https://doi.org/10.1007/978-0-387-34768-4_19
    63 rdf:type schema:CreativeWork
    64 sg:pub.10.1007/bf00244283 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024762168
    65 https://doi.org/10.1007/bf00244283
    66 rdf:type schema:CreativeWork
    67 https://www.grid.ac/institutes/grid.266832.b schema:alternateName University of New Mexico
    68 schema:name University of New Mexico, 87131, Albuquerque, NM, U.S.A
    69 rdf:type schema:Organization
     




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


    ...