Generating Minimal Herbrand Models Step by Step View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

1999

AUTHORS

Heribert Schütz

ABSTRACT

This paper presents a way to improve minimal model generation for clausal theories. It works by breaking up the model generation process into several steps according to several parts of the given theory. It is shown that elimination of non-minimal or duplicate models can be performed after each step, which reduces the overall search space. An even stronger reduction of the search space is possible if we are interested only in certain parts of the models to be generated. The techniques are applicable to any method for the generation of minimal Herbrand models. The paper goes into some detail how they can be integrated tightly into the PUHR tableau method. More... »

PAGES

263-277

References to SciGraph publications

  • 1995-06. SATCHMORE: SATCHMO with RElevancy in JOURNAL OF AUTOMATED REASONING
  • 1988. SATCHMO: A theorem prover implemented in Prolog in 9TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
  • 2005-06-17. Tableaux for diagnosis applications in AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS
  • Book

    TITLE

    Automated Reasoning with Analytic Tableaux and Related Methods

    ISBN

    978-3-540-66086-6
    978-3-540-48754-8

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/3-540-48754-9_23

    DOI

    http://dx.doi.org/10.1007/3-540-48754-9_23

    DIMENSIONS

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


    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/0102", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Applied Mathematics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/01", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Mathematical Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Ludwig Maximilian University of Munich", 
              "id": "https://www.grid.ac/institutes/grid.5252.0", 
              "name": [
                "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Germany"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Sch\u00fctz", 
            "givenName": "Heribert", 
            "id": "sg:person.07726356155.42", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07726356155.42"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1145/321250.321253", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1009195371"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00881861", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1023028400", 
              "https://doi.org/10.1007/bf00881861"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0027406", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027257592", 
              "https://doi.org/10.1007/bfb0027406"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0027406", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027257592", 
              "https://doi.org/10.1007/bfb0027406"
            ], 
            "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": "https://doi.org/10.1016/s0743-1066(96)00116-1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1048929603"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1999", 
        "datePublishedReg": "1999-01-01", 
        "description": "This paper presents a way to improve minimal model generation for clausal theories. It works by breaking up the model generation process into several steps according to several parts of the given theory. It is shown that elimination of non-minimal or duplicate models can be performed after each step, which reduces the overall search space. An even stronger reduction of the search space is possible if we are interested only in certain parts of the models to be generated. The techniques are applicable to any method for the generation of minimal Herbrand models. The paper goes into some detail how they can be integrated tightly into the PUHR tableau method.", 
        "editor": [
          {
            "familyName": "Murray", 
            "givenName": "Neil V.", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/3-540-48754-9_23", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-540-66086-6", 
            "978-3-540-48754-8"
          ], 
          "name": "Automated Reasoning with Analytic Tableaux and Related Methods", 
          "type": "Book"
        }, 
        "name": "Generating Minimal Herbrand Models Step by Step", 
        "pagination": "263-277", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/3-540-48754-9_23"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "50c5e1f19f42a05911dd5e13a1fc4ca43e3cd494fb7a02914d5578b48b01f62b"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1016953105"
            ]
          }
        ], 
        "publisher": {
          "location": "Berlin, Heidelberg", 
          "name": "Springer Berlin Heidelberg", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/3-540-48754-9_23", 
          "https://app.dimensions.ai/details/publication/pub.1016953105"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-15T23:51", 
        "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_8697_00000253.jsonl", 
        "type": "Chapter", 
        "url": "http://link.springer.com/10.1007/3-540-48754-9_23"
      }
    ]
     

    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/3-540-48754-9_23'

    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/3-540-48754-9_23'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-48754-9_23'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/3-540-48754-9_23'


     

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

    83 TRIPLES      23 PREDICATES      32 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/3-540-48754-9_23 schema:about anzsrc-for:01
    2 anzsrc-for:0102
    3 schema:author Ncee37cd66d2f4bf8a507b6e02b54058c
    4 schema:citation sg:pub.10.1007/bf00881861
    5 sg:pub.10.1007/bfb0012847
    6 sg:pub.10.1007/bfb0027406
    7 https://doi.org/10.1016/s0743-1066(96)00116-1
    8 https://doi.org/10.1145/321250.321253
    9 schema:datePublished 1999
    10 schema:datePublishedReg 1999-01-01
    11 schema:description This paper presents a way to improve minimal model generation for clausal theories. It works by breaking up the model generation process into several steps according to several parts of the given theory. It is shown that elimination of non-minimal or duplicate models can be performed after each step, which reduces the overall search space. An even stronger reduction of the search space is possible if we are interested only in certain parts of the models to be generated. The techniques are applicable to any method for the generation of minimal Herbrand models. The paper goes into some detail how they can be integrated tightly into the PUHR tableau method.
    12 schema:editor N16ac792a57434ea59269c427658535ab
    13 schema:genre chapter
    14 schema:inLanguage en
    15 schema:isAccessibleForFree false
    16 schema:isPartOf Na76ba6ed939f4e7aad708ee0066b8f58
    17 schema:name Generating Minimal Herbrand Models Step by Step
    18 schema:pagination 263-277
    19 schema:productId N525e6624df3744e9b40d0803d2f6b471
    20 Nb0c0467a92424f19a946e13188e9782d
    21 Nc7004c2a666c4e7eb1cd0db39ebe7906
    22 schema:publisher Na4fa1c3fd6bf44d1b1dea0ba7767867b
    23 schema:sameAs https://app.dimensions.ai/details/publication/pub.1016953105
    24 https://doi.org/10.1007/3-540-48754-9_23
    25 schema:sdDatePublished 2019-04-15T23:51
    26 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    27 schema:sdPublisher N8989acfb0e7a448794ae4464019a2b03
    28 schema:url http://link.springer.com/10.1007/3-540-48754-9_23
    29 sgo:license sg:explorer/license/
    30 sgo:sdDataset chapters
    31 rdf:type schema:Chapter
    32 N16ac792a57434ea59269c427658535ab rdf:first N83e6b2e6506b476eadd4f8a781255b85
    33 rdf:rest rdf:nil
    34 N525e6624df3744e9b40d0803d2f6b471 schema:name doi
    35 schema:value 10.1007/3-540-48754-9_23
    36 rdf:type schema:PropertyValue
    37 N83e6b2e6506b476eadd4f8a781255b85 schema:familyName Murray
    38 schema:givenName Neil V.
    39 rdf:type schema:Person
    40 N8989acfb0e7a448794ae4464019a2b03 schema:name Springer Nature - SN SciGraph project
    41 rdf:type schema:Organization
    42 Na4fa1c3fd6bf44d1b1dea0ba7767867b schema:location Berlin, Heidelberg
    43 schema:name Springer Berlin Heidelberg
    44 rdf:type schema:Organisation
    45 Na76ba6ed939f4e7aad708ee0066b8f58 schema:isbn 978-3-540-48754-8
    46 978-3-540-66086-6
    47 schema:name Automated Reasoning with Analytic Tableaux and Related Methods
    48 rdf:type schema:Book
    49 Nb0c0467a92424f19a946e13188e9782d schema:name readcube_id
    50 schema:value 50c5e1f19f42a05911dd5e13a1fc4ca43e3cd494fb7a02914d5578b48b01f62b
    51 rdf:type schema:PropertyValue
    52 Nc7004c2a666c4e7eb1cd0db39ebe7906 schema:name dimensions_id
    53 schema:value pub.1016953105
    54 rdf:type schema:PropertyValue
    55 Ncee37cd66d2f4bf8a507b6e02b54058c rdf:first sg:person.07726356155.42
    56 rdf:rest rdf:nil
    57 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
    58 schema:name Mathematical Sciences
    59 rdf:type schema:DefinedTerm
    60 anzsrc-for:0102 schema:inDefinedTermSet anzsrc-for:
    61 schema:name Applied Mathematics
    62 rdf:type schema:DefinedTerm
    63 sg:person.07726356155.42 schema:affiliation https://www.grid.ac/institutes/grid.5252.0
    64 schema:familyName Schütz
    65 schema:givenName Heribert
    66 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07726356155.42
    67 rdf:type schema:Person
    68 sg:pub.10.1007/bf00881861 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023028400
    69 https://doi.org/10.1007/bf00881861
    70 rdf:type schema:CreativeWork
    71 sg:pub.10.1007/bfb0012847 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031681210
    72 https://doi.org/10.1007/bfb0012847
    73 rdf:type schema:CreativeWork
    74 sg:pub.10.1007/bfb0027406 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027257592
    75 https://doi.org/10.1007/bfb0027406
    76 rdf:type schema:CreativeWork
    77 https://doi.org/10.1016/s0743-1066(96)00116-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1048929603
    78 rdf:type schema:CreativeWork
    79 https://doi.org/10.1145/321250.321253 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009195371
    80 rdf:type schema:CreativeWork
    81 https://www.grid.ac/institutes/grid.5252.0 schema:alternateName Ludwig Maximilian University of Munich
    82 schema:name Institut für Informatik, Universität München, Germany
    83 rdf:type schema:Organization
     




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


    ...