Using hints to increase the effectiveness of an automated reasoning program: Case studies View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1996-06

AUTHORS

Robert Veroff

ABSTRACT

In this article we consider the use of hints to help guide the search for a proof. Under the hints strategy, the value of a generated clause is determined, in part, by whether or not the clause subsumes or is subsumed by a user-supplied hint clause. We have implemented the hints strategy and have experimented with it extensively. We summarize our experiences for a variety of reasoning tasks, including proof checking, proof completion, and proof finding. We conclude that the hints strategy has value beyond simply “giving the proof to find the proof.” More... »

PAGES

223-239

References to SciGraph publications

  • 1991. Automated Reasoning and Bledsoe’s Dream for the Field in AUTOMATED REASONING
  • 1990-12. Robbins algebra: Conditions that make a near-boolean algebra boolean in JOURNAL OF AUTOMATED REASONING
  • 1992-04. The linked inference principle, I: The formal treatment in JOURNAL OF AUTOMATED REASONING
  • 1990-06. Meeting the challenge of fifty years of logic in JOURNAL OF AUTOMATED REASONING
  • 1987-12. Case studies of Z-module reasoning: Proving benchmark theorems from ring theory in JOURNAL OF AUTOMATED REASONING
  • Identifiers

    URI

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

    DOI

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

    DIMENSIONS

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


    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/1117", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Public Health and Health Services", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/11", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Medical and Health 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, USA"
              ], 
              "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-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": "sg:pub.10.1007/bf00247439", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008726187", 
              "https://doi.org/10.1007/bf00247439"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00247439", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008726187", 
              "https://doi.org/10.1007/bf00247439"
            ], 
            "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/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(77)90012-1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027513096"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0004-3702(77)90012-1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027513096"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00245821", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043944288", 
              "https://doi.org/10.1007/bf00245821"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00245821", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043944288", 
              "https://doi.org/10.1007/bf00245821"
            ], 
            "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/bf00244359", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1048595116", 
              "https://doi.org/10.1007/bf00244359"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00244359", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1048595116", 
              "https://doi.org/10.1007/bf00244359"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1996-06", 
        "datePublishedReg": "1996-06-01", 
        "description": "In this article we consider the use of hints to help guide the search for a proof. Under the hints strategy, the value of a generated clause is determined, in part, by whether or not the clause subsumes or is subsumed by a user-supplied hint clause. We have implemented the hints strategy and have experimented with it extensively. We summarize our experiences for a variety of reasoning tasks, including proof checking, proof completion, and proof finding. We conclude that the hints strategy has value beyond simply \u201cgiving the proof to find the proof.\u201d", 
        "genre": "research_article", 
        "id": "sg:pub.10.1007/bf00252178", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1136522", 
            "issn": [
              "0168-7433", 
              "1573-0670"
            ], 
            "name": "Journal of Automated Reasoning", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "3", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "16"
          }
        ], 
        "name": "Using hints to increase the effectiveness of an automated reasoning program: Case studies", 
        "pagination": "223-239", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "1cc8af05d2f1ab0bbf15fb878b815b4153d1f4e0b27e23353994e4de02e4de08"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/bf00252178"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1006042548"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/bf00252178", 
          "https://app.dimensions.ai/details/publication/pub.1006042548"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-11T14:01", 
        "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/0000000371_0000000371/records_130830_00000000.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "http://link.springer.com/10.1007/BF00252178"
      }
    ]
     

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

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

    Turtle is a human-readable linked data format.

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

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

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


     

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

    90 TRIPLES      21 PREDICATES      35 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/bf00252178 schema:about anzsrc-for:11
    2 anzsrc-for:1117
    3 schema:author N4daae3d84b404f22acb70e22f0bbebf4
    4 schema:citation sg:pub.10.1007/978-94-011-3488-0_15
    5 sg:pub.10.1007/bf00244283
    6 sg:pub.10.1007/bf00244359
    7 sg:pub.10.1007/bf00245821
    8 sg:pub.10.1007/bf00247439
    9 https://doi.org/10.1016/0004-3702(77)90012-1
    10 https://doi.org/10.1016/0898-1221(76)90002-x
    11 https://doi.org/10.1016/0898-1221(94)00220-f
    12 schema:datePublished 1996-06
    13 schema:datePublishedReg 1996-06-01
    14 schema:description In this article we consider the use of hints to help guide the search for a proof. Under the hints strategy, the value of a generated clause is determined, in part, by whether or not the clause subsumes or is subsumed by a user-supplied hint clause. We have implemented the hints strategy and have experimented with it extensively. We summarize our experiences for a variety of reasoning tasks, including proof checking, proof completion, and proof finding. We conclude that the hints strategy has value beyond simply “giving the proof to find the proof.”
    15 schema:genre research_article
    16 schema:inLanguage en
    17 schema:isAccessibleForFree false
    18 schema:isPartOf N7ca564924c804778893cd73ac23fb3b9
    19 Ne25b5d3a31f84bd3bf3330786bbdce53
    20 sg:journal.1136522
    21 schema:name Using hints to increase the effectiveness of an automated reasoning program: Case studies
    22 schema:pagination 223-239
    23 schema:productId N951ff1404cc4407782066118c29a3232
    24 Nca38a2b4dc2d4a2ca9c3c4dd66867eed
    25 Nfca95d50b09841499290974c86093bc6
    26 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006042548
    27 https://doi.org/10.1007/bf00252178
    28 schema:sdDatePublished 2019-04-11T14:01
    29 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    30 schema:sdPublisher Nf9ad1926606d4a00833d1a7800114543
    31 schema:url http://link.springer.com/10.1007/BF00252178
    32 sgo:license sg:explorer/license/
    33 sgo:sdDataset articles
    34 rdf:type schema:ScholarlyArticle
    35 N4daae3d84b404f22acb70e22f0bbebf4 rdf:first sg:person.0644424756.64
    36 rdf:rest rdf:nil
    37 N7ca564924c804778893cd73ac23fb3b9 schema:issueNumber 3
    38 rdf:type schema:PublicationIssue
    39 N951ff1404cc4407782066118c29a3232 schema:name readcube_id
    40 schema:value 1cc8af05d2f1ab0bbf15fb878b815b4153d1f4e0b27e23353994e4de02e4de08
    41 rdf:type schema:PropertyValue
    42 Nca38a2b4dc2d4a2ca9c3c4dd66867eed schema:name dimensions_id
    43 schema:value pub.1006042548
    44 rdf:type schema:PropertyValue
    45 Ne25b5d3a31f84bd3bf3330786bbdce53 schema:volumeNumber 16
    46 rdf:type schema:PublicationVolume
    47 Nf9ad1926606d4a00833d1a7800114543 schema:name Springer Nature - SN SciGraph project
    48 rdf:type schema:Organization
    49 Nfca95d50b09841499290974c86093bc6 schema:name doi
    50 schema:value 10.1007/bf00252178
    51 rdf:type schema:PropertyValue
    52 anzsrc-for:11 schema:inDefinedTermSet anzsrc-for:
    53 schema:name Medical and Health Sciences
    54 rdf:type schema:DefinedTerm
    55 anzsrc-for:1117 schema:inDefinedTermSet anzsrc-for:
    56 schema:name Public Health and Health Services
    57 rdf:type schema:DefinedTerm
    58 sg:journal.1136522 schema:issn 0168-7433
    59 1573-0670
    60 schema:name Journal of Automated Reasoning
    61 rdf:type schema:Periodical
    62 sg:person.0644424756.64 schema:affiliation https://www.grid.ac/institutes/grid.266832.b
    63 schema:familyName Veroff
    64 schema:givenName Robert
    65 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0644424756.64
    66 rdf:type schema:Person
    67 sg:pub.10.1007/978-94-011-3488-0_15 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008246432
    68 https://doi.org/10.1007/978-94-011-3488-0_15
    69 rdf:type schema:CreativeWork
    70 sg:pub.10.1007/bf00244283 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024762168
    71 https://doi.org/10.1007/bf00244283
    72 rdf:type schema:CreativeWork
    73 sg:pub.10.1007/bf00244359 schema:sameAs https://app.dimensions.ai/details/publication/pub.1048595116
    74 https://doi.org/10.1007/bf00244359
    75 rdf:type schema:CreativeWork
    76 sg:pub.10.1007/bf00245821 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043944288
    77 https://doi.org/10.1007/bf00245821
    78 rdf:type schema:CreativeWork
    79 sg:pub.10.1007/bf00247439 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008726187
    80 https://doi.org/10.1007/bf00247439
    81 rdf:type schema:CreativeWork
    82 https://doi.org/10.1016/0004-3702(77)90012-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027513096
    83 rdf:type schema:CreativeWork
    84 https://doi.org/10.1016/0898-1221(76)90002-x schema:sameAs https://app.dimensions.ai/details/publication/pub.1044945425
    85 rdf:type schema:CreativeWork
    86 https://doi.org/10.1016/0898-1221(94)00220-f schema:sameAs https://app.dimensions.ai/details/publication/pub.1012294032
    87 rdf:type schema:CreativeWork
    88 https://www.grid.ac/institutes/grid.266832.b schema:alternateName University of New Mexico
    89 schema:name University of New Mexico, 87131, Albuquerque, NM, USA
    90 rdf:type schema:Organization
     




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


    ...