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 Nbe51846d67c14c0c98f59a01336949b1
    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 N8f5209996aff4b50965c7032f466ce68
    17 N94af6694e4c542e4b68619b88051d7fc
    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 N89f02d2c848c4d63bab13ddf700b8785
    61 N98a8a052df14441c974c566fba34cb65
    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 N839c5417b29840638f45d38c74a9a653
    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 N24afdef45e7e409b83fb26b9fceec8ea rdf:first N2aeca26edf534f1e857dc4828b416a47
    72 rdf:rest rdf:nil
    73 N2aeca26edf534f1e857dc4828b416a47 schema:affiliation grid-institutes:grid.26009.3d
    74 schema:familyName Wilson
    75 schema:givenName Debra S.
    76 rdf:type schema:Person
    77 N839c5417b29840638f45d38c74a9a653 schema:name Springer Nature - SN SciGraph project
    78 rdf:type schema:Organization
    79 N89f02d2c848c4d63bab13ddf700b8785 schema:name dimensions_id
    80 schema:value pub.1023028400
    81 rdf:type schema:PropertyValue
    82 N8f5209996aff4b50965c7032f466ce68 schema:volumeNumber 14
    83 rdf:type schema:PublicationVolume
    84 N94af6694e4c542e4b68619b88051d7fc schema:issueNumber 2
    85 rdf:type schema:PublicationIssue
    86 N98a8a052df14441c974c566fba34cb65 schema:name doi
    87 schema:value 10.1007/bf00881861
    88 rdf:type schema:PropertyValue
    89 Nbe51846d67c14c0c98f59a01336949b1 rdf:first sg:person.015355674335.16
    90 rdf:rest Ne0bb9180bee64397bf721d47b94bca9b
    91 Ne0bb9180bee64397bf721d47b94bca9b rdf:first sg:person.016001231167.57
    92 rdf:rest N24afdef45e7e409b83fb26b9fceec8ea
    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)


    ...