SATCHMORE: SATCHMO with RElevancy View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1995-06

AUTHORS

Donald W. Loveland, David W. Reed, Debra S. Wilson

ABSTRACT

We introduce a relevancy detection algorithm to be used in conjunction with the SATCHMO prover. The version of SATCHMO considered here is essentially a bidirectional prover, utilizing Prolog (back chaining) on Horn clauses and forward chaining on non-Horn clauses. Our extension, SATCHMORE (SATCHMO with RElevancy), addresses the major weakness of SATCHMO: the uncontrolled use of forward chaining. By marking potentially relevant clause head literals, and then requiring that all the head literals be marked relevant (be “totally relevant”) before a clause is used for forward chaining, SATCHMORE is able to guide the use of these rules. Furthermore, the relevancy testing is performed without extending the proof search beyond what is done in SATCHMO. A simple implementation of the extended SATCHMO can be written in Prolog. We describe our relevancy testing approach, present the implementation, prove soundness and completeness, and provide examples that demonstrate the power of relevancy testing. More... »

PAGES

325-351

References to SciGraph publications

  • 1992. The near-Horn approach to disjunctive logic programming in EXTENSIONS OF LOGIC PROGRAMMING
  • 1987. Foundations of Logic Programming in NONE
  • 1988. SATCHMO: A theorem prover implemented in Prolog in 9TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
  • 1994-06. Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction in JOURNAL OF AUTOMATED REASONING
  • 1986-03. Schubert's Steamroller problem: Formulations and solutions in JOURNAL OF AUTOMATED REASONING
  • 1991-09. Generating relevant models in JOURNAL OF AUTOMATED REASONING
  • Identifiers

    URI

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

    DOI

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

    DIMENSIONS

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


    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/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Artificial Intelligence and Image Processing", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Department of Computer Science, Duke University, 27708, Durham, NC", 
              "id": "http://www.grid.ac/institutes/grid.26009.3d", 
              "name": [
                "Department of Computer Science, Duke University, 27708, Durham, NC"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Loveland", 
            "givenName": "Donald W.", 
            "id": "sg:person.015355674335.16", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015355674335.16"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Department of Computer Science, Duke University, 27708, Durham, NC", 
              "id": "http://www.grid.ac/institutes/grid.26009.3d", 
              "name": [
                "Department of Computer Science, Duke University, 27708, Durham, NC"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Reed", 
            "givenName": "David W.", 
            "id": "sg:person.016001231167.57", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016001231167.57"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Department of Computer Science, Duke University, 27708, Durham, NC", 
              "id": "http://www.grid.ac/institutes/grid.26009.3d", 
              "name": [
                "Department of Computer Science, Duke University, 27708, Durham, NC"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Wilson", 
            "givenName": "Debra S.", 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/bf00249019", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007249279", 
              "https://doi.org/10.1007/bf00249019"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00881955", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039391289", 
              "https://doi.org/10.1007/bf00881955"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-83189-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1016029570", 
              "https://doi.org/10.1007/978-3-642-83189-8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0012847", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1031681210", 
              "https://doi.org/10.1007/bfb0012847"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00246025", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010797831", 
              "https://doi.org/10.1007/bf00246025"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0013613", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1042018755", 
              "https://doi.org/10.1007/bfb0013613"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1995-06", 
        "datePublishedReg": "1995-06-01", 
        "description": "We introduce a relevancy detection algorithm to be used in conjunction with the SATCHMO prover. The version of SATCHMO considered here is essentially a bidirectional prover, utilizing Prolog (back chaining) on Horn clauses and forward chaining on non-Horn clauses. Our extension, SATCHMORE (SATCHMO with RElevancy), addresses the major weakness of SATCHMO: the uncontrolled use of forward chaining. By marking potentially relevant clause head literals, and then requiring that all the head literals be marked relevant (be \u201ctotally relevant\u201d) before a clause is used for forward chaining, SATCHMORE is able to guide the use of these rules. Furthermore, the relevancy testing is performed without extending the proof search beyond what is done in SATCHMO. A simple implementation of the extended SATCHMO can be written in Prolog. We describe our relevancy testing approach, present the implementation, prove soundness and completeness, and provide examples that demonstrate the power of relevancy testing.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/bf00881861", 
        "inLanguage": "en", 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1136522", 
            "issn": [
              "0168-7433", 
              "1573-0670"
            ], 
            "name": "Journal of Automated Reasoning", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "14"
          }
        ], 
        "keywords": [
          "relevancy testing", 
          "head literals", 
          "proof search", 
          "detection algorithm", 
          "Horn clauses", 
          "non-Horn clauses", 
          "simple implementation", 
          "testing approach", 
          "Prolog", 
          "SATCHMO", 
          "implementation", 
          "literals", 
          "provers", 
          "major weakness", 
          "algorithm", 
          "SATCHMORE", 
          "soundness", 
          "clauses", 
          "relevancy", 
          "rules", 
          "search", 
          "completeness", 
          "version", 
          "extension", 
          "example", 
          "use", 
          "testing", 
          "weakness", 
          "power", 
          "conjunction", 
          "uncontrolled use", 
          "approach", 
          "relevancy detection algorithm", 
          "version of SATCHMO", 
          "bidirectional prover", 
          "relevant clause head literals", 
          "clause head literals", 
          "extended SATCHMO", 
          "relevancy testing approach"
        ], 
        "name": "SATCHMORE: SATCHMO with RElevancy", 
        "pagination": "325-351", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1023028400"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/bf00881861"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/bf00881861", 
          "https://app.dimensions.ai/details/publication/pub.1023028400"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2021-12-01T19:10", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/article/article_283.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/bf00881861"
      }
    ]
     

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

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

    Turtle is a human-readable linked data format.

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

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

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


     

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

    134 TRIPLES      22 PREDICATES      71 URIs      57 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/bf00881861 schema:about anzsrc-for:08
    2 anzsrc-for:0801
    3 schema:author Nb389ff6af3f4401fa6ded7e3bcc76685
    4 schema:citation sg:pub.10.1007/978-3-642-83189-8
    5 sg:pub.10.1007/bf00246025
    6 sg:pub.10.1007/bf00249019
    7 sg:pub.10.1007/bf00881955
    8 sg:pub.10.1007/bfb0012847
    9 sg:pub.10.1007/bfb0013613
    10 schema:datePublished 1995-06
    11 schema:datePublishedReg 1995-06-01
    12 schema:description We introduce a relevancy detection algorithm to be used in conjunction with the SATCHMO prover. The version of SATCHMO considered here is essentially a bidirectional prover, utilizing Prolog (back chaining) on Horn clauses and forward chaining on non-Horn clauses. Our extension, SATCHMORE (SATCHMO with RElevancy), addresses the major weakness of SATCHMO: the uncontrolled use of forward chaining. By marking potentially relevant clause head literals, and then requiring that all the head literals be marked relevant (be “totally relevant”) before a clause is used for forward chaining, SATCHMORE is able to guide the use of these rules. Furthermore, the relevancy testing is performed without extending the proof search beyond what is done in SATCHMO. A simple implementation of the extended SATCHMO can be written in Prolog. We describe our relevancy testing approach, present the implementation, prove soundness and completeness, and provide examples that demonstrate the power of relevancy testing.
    13 schema:genre article
    14 schema:inLanguage en
    15 schema:isAccessibleForFree false
    16 schema:isPartOf N6638579acd3d46049b503886279b20de
    17 Ndd229c603ee74597b4fc392097485035
    18 sg:journal.1136522
    19 schema:keywords Horn clauses
    20 Prolog
    21 SATCHMO
    22 SATCHMORE
    23 algorithm
    24 approach
    25 bidirectional prover
    26 clause head literals
    27 clauses
    28 completeness
    29 conjunction
    30 detection algorithm
    31 example
    32 extended SATCHMO
    33 extension
    34 head literals
    35 implementation
    36 literals
    37 major weakness
    38 non-Horn clauses
    39 power
    40 proof search
    41 provers
    42 relevancy
    43 relevancy detection algorithm
    44 relevancy testing
    45 relevancy testing approach
    46 relevant clause head literals
    47 rules
    48 search
    49 simple implementation
    50 soundness
    51 testing
    52 testing approach
    53 uncontrolled use
    54 use
    55 version
    56 version of SATCHMO
    57 weakness
    58 schema:name SATCHMORE: SATCHMO with RElevancy
    59 schema:pagination 325-351
    60 schema:productId N32521d8f5ff04a89a0c21ecd681c31ab
    61 N893d600d0a604349a32d68eca887407a
    62 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023028400
    63 https://doi.org/10.1007/bf00881861
    64 schema:sdDatePublished 2021-12-01T19:10
    65 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    66 schema:sdPublisher N3dbf82062bae4739964dec23b9673eaf
    67 schema:url https://doi.org/10.1007/bf00881861
    68 sgo:license sg:explorer/license/
    69 sgo:sdDataset articles
    70 rdf:type schema:ScholarlyArticle
    71 N111c00e5f0d64edbb81ed762d8b4cf57 rdf:first sg:person.016001231167.57
    72 rdf:rest Ne7b90c81102d4eb4876db9493fc744b6
    73 N2e63594b62e8427986ed38030495e2e4 schema:affiliation grid-institutes:grid.26009.3d
    74 schema:familyName Wilson
    75 schema:givenName Debra S.
    76 rdf:type schema:Person
    77 N32521d8f5ff04a89a0c21ecd681c31ab schema:name dimensions_id
    78 schema:value pub.1023028400
    79 rdf:type schema:PropertyValue
    80 N3dbf82062bae4739964dec23b9673eaf schema:name Springer Nature - SN SciGraph project
    81 rdf:type schema:Organization
    82 N6638579acd3d46049b503886279b20de schema:issueNumber 2
    83 rdf:type schema:PublicationIssue
    84 N893d600d0a604349a32d68eca887407a schema:name doi
    85 schema:value 10.1007/bf00881861
    86 rdf:type schema:PropertyValue
    87 Nb389ff6af3f4401fa6ded7e3bcc76685 rdf:first sg:person.015355674335.16
    88 rdf:rest N111c00e5f0d64edbb81ed762d8b4cf57
    89 Ndd229c603ee74597b4fc392097485035 schema:volumeNumber 14
    90 rdf:type schema:PublicationVolume
    91 Ne7b90c81102d4eb4876db9493fc744b6 rdf:first N2e63594b62e8427986ed38030495e2e4
    92 rdf:rest rdf:nil
    93 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    94 schema:name Information and Computing Sciences
    95 rdf:type schema:DefinedTerm
    96 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
    97 schema:name Artificial Intelligence and Image Processing
    98 rdf:type schema:DefinedTerm
    99 sg:journal.1136522 schema:issn 0168-7433
    100 1573-0670
    101 schema:name Journal of Automated Reasoning
    102 schema:publisher Springer Nature
    103 rdf:type schema:Periodical
    104 sg:person.015355674335.16 schema:affiliation grid-institutes:grid.26009.3d
    105 schema:familyName Loveland
    106 schema:givenName Donald W.
    107 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015355674335.16
    108 rdf:type schema:Person
    109 sg:person.016001231167.57 schema:affiliation grid-institutes:grid.26009.3d
    110 schema:familyName Reed
    111 schema:givenName David W.
    112 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016001231167.57
    113 rdf:type schema:Person
    114 sg:pub.10.1007/978-3-642-83189-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1016029570
    115 https://doi.org/10.1007/978-3-642-83189-8
    116 rdf:type schema:CreativeWork
    117 sg:pub.10.1007/bf00246025 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010797831
    118 https://doi.org/10.1007/bf00246025
    119 rdf:type schema:CreativeWork
    120 sg:pub.10.1007/bf00249019 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007249279
    121 https://doi.org/10.1007/bf00249019
    122 rdf:type schema:CreativeWork
    123 sg:pub.10.1007/bf00881955 schema:sameAs https://app.dimensions.ai/details/publication/pub.1039391289
    124 https://doi.org/10.1007/bf00881955
    125 rdf:type schema:CreativeWork
    126 sg:pub.10.1007/bfb0012847 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031681210
    127 https://doi.org/10.1007/bfb0012847
    128 rdf:type schema:CreativeWork
    129 sg:pub.10.1007/bfb0013613 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042018755
    130 https://doi.org/10.1007/bfb0013613
    131 rdf:type schema:CreativeWork
    132 grid-institutes:grid.26009.3d schema:alternateName Department of Computer Science, Duke University, 27708, Durham, NC
    133 schema:name Department of Computer Science, Duke University, 27708, Durham, NC
    134 rdf:type schema:Organization
     




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


    ...