Efficient model generation through compilation View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

1996

AUTHORS

Heribert Schütz , Tim Geisler

ABSTRACT

We present a collection of simple but powerful techniques for enhancing the efficiency of model-generation theorem provers such as Satchmo. The central ideas are to compile a clausal first order theory into a procedural Prolog program and to avoid redundant work of a naïve implementation. We also give an efficient implementation for complement splitting, a method for minimizing the first generated model and for pruning the search space. Furthermore we show that it is not efficient to ensure fair selection of clauses by a purely breadth-first search strategy and present a significantly more efficient strategy. We have compared various combinations of our techniques among each other and with the theorem provers MGTP/G, Otter, and SETHEO, using the TPTP Problem Library as a benchmark. Our implementation has turned out to be the most efficient for range-restricted problems and for a class of problems we call “non-nesting”. More... »

PAGES

433-447

References to SciGraph publications

Book

TITLE

Automated Deduction — Cade-13

ISBN

978-3-540-61511-8
978-3-540-68687-3

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/3-540-61511-3_105

DOI

http://dx.doi.org/10.1007/3-540-61511-3_105

DIMENSIONS

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


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/0103", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Numerical and Computational 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": {
          "name": [
            "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Oettingenstr. 67, D-80538\u00a0M\u00fcnchen"
          ], 
          "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"
      }, 
      {
        "affiliation": {
          "name": [
            "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Oettingenstr. 67, D-80538\u00a0M\u00fcnchen"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Geisler", 
        "givenName": "Tim", 
        "id": "sg:person.012116677555.81", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012116677555.81"
        ], 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "https://doi.org/10.1016/0004-3702(82)90020-0", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1013363801"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0004-3702(82)90020-0", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1013363801"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf00297245", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1034625725", 
          "https://doi.org/10.1007/bf00297245"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf00297245", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1034625725", 
          "https://doi.org/10.1007/bf00297245"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "1996", 
    "datePublishedReg": "1996-01-01", 
    "description": "We present a collection of simple but powerful techniques for enhancing the efficiency of model-generation theorem provers such as Satchmo. The central ideas are to compile a clausal first order theory into a procedural Prolog program and to avoid redundant work of a na\u00efve implementation. We also give an efficient implementation for complement splitting, a method for minimizing the first generated model and for pruning the search space. Furthermore we show that it is not efficient to ensure fair selection of clauses by a purely breadth-first search strategy and present a significantly more efficient strategy. We have compared various combinations of our techniques among each other and with the theorem provers MGTP/G, Otter, and SETHEO, using the TPTP Problem Library as a benchmark. Our implementation has turned out to be the most efficient for range-restricted problems and for a class of problems we call \u201cnon-nesting\u201d.", 
    "editor": [
      {
        "familyName": "McRobbie", 
        "givenName": "M. A.", 
        "type": "Person"
      }, 
      {
        "familyName": "Slaney", 
        "givenName": "J. K.", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/3-540-61511-3_105", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-61511-8", 
        "978-3-540-68687-3"
      ], 
      "name": "Automated Deduction \u2014 Cade-13", 
      "type": "Book"
    }, 
    "name": "Efficient model generation through compilation", 
    "pagination": "433-447", 
    "productId": [
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/3-540-61511-3_105"
        ]
      }, 
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "fbbb1c25ce8ede6b1fddc50a9e7cebc8d1c487ac9d3f1b5b0ddf494222a684ed"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1052848223"
        ]
      }
    ], 
    "publisher": {
      "location": "Berlin, Heidelberg", 
      "name": "Springer Berlin Heidelberg", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/3-540-61511-3_105", 
      "https://app.dimensions.ai/details/publication/pub.1052848223"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2019-04-16T00:52", 
    "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_8700_00000276.jsonl", 
    "type": "Chapter", 
    "url": "http://link.springer.com/10.1007/3-540-61511-3_105"
  }
]
 

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-61511-3_105'

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-61511-3_105'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-61511-3_105'

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-61511-3_105'


 

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

85 TRIPLES      23 PREDICATES      29 URIs      20 LITERALS      8 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/3-540-61511-3_105 schema:about anzsrc-for:01
2 anzsrc-for:0103
3 schema:author N0d2d106a2ca142a98e31a012e86e99ea
4 schema:citation sg:pub.10.1007/bf00297245
5 https://doi.org/10.1016/0004-3702(82)90020-0
6 schema:datePublished 1996
7 schema:datePublishedReg 1996-01-01
8 schema:description We present a collection of simple but powerful techniques for enhancing the efficiency of model-generation theorem provers such as Satchmo. The central ideas are to compile a clausal first order theory into a procedural Prolog program and to avoid redundant work of a naïve implementation. We also give an efficient implementation for complement splitting, a method for minimizing the first generated model and for pruning the search space. Furthermore we show that it is not efficient to ensure fair selection of clauses by a purely breadth-first search strategy and present a significantly more efficient strategy. We have compared various combinations of our techniques among each other and with the theorem provers MGTP/G, Otter, and SETHEO, using the TPTP Problem Library as a benchmark. Our implementation has turned out to be the most efficient for range-restricted problems and for a class of problems we call “non-nesting”.
9 schema:editor N9f8bdfb6799a47fb9e5b41a577785e57
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf N96d7c890684c4826888cbfea434cf08e
14 schema:name Efficient model generation through compilation
15 schema:pagination 433-447
16 schema:productId N34e210b727ec4e189fc28563f23f4fbb
17 N3d0f77346e1a4488934fc4e4d13ba458
18 N590a6ddf3bcc45db8db4bf5993b53b69
19 schema:publisher N82c09027438c44cba055bf5d5cf9d44e
20 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052848223
21 https://doi.org/10.1007/3-540-61511-3_105
22 schema:sdDatePublished 2019-04-16T00:52
23 schema:sdLicense https://scigraph.springernature.com/explorer/license/
24 schema:sdPublisher N15ba4d786941443d8a21933050ba3274
25 schema:url http://link.springer.com/10.1007/3-540-61511-3_105
26 sgo:license sg:explorer/license/
27 sgo:sdDataset chapters
28 rdf:type schema:Chapter
29 N0d2d106a2ca142a98e31a012e86e99ea rdf:first sg:person.07726356155.42
30 rdf:rest Na59f1b2d7ecb4fb0890203015698cb1f
31 N15ba4d786941443d8a21933050ba3274 schema:name Springer Nature - SN SciGraph project
32 rdf:type schema:Organization
33 N34e210b727ec4e189fc28563f23f4fbb schema:name dimensions_id
34 schema:value pub.1052848223
35 rdf:type schema:PropertyValue
36 N39faf7aff99c4ef6a6331fdffa0970da schema:familyName McRobbie
37 schema:givenName M. A.
38 rdf:type schema:Person
39 N3d0f77346e1a4488934fc4e4d13ba458 schema:name readcube_id
40 schema:value fbbb1c25ce8ede6b1fddc50a9e7cebc8d1c487ac9d3f1b5b0ddf494222a684ed
41 rdf:type schema:PropertyValue
42 N4099b164e60b4a98a15539b0fa20ee67 schema:familyName Slaney
43 schema:givenName J. K.
44 rdf:type schema:Person
45 N590a6ddf3bcc45db8db4bf5993b53b69 schema:name doi
46 schema:value 10.1007/3-540-61511-3_105
47 rdf:type schema:PropertyValue
48 N82c09027438c44cba055bf5d5cf9d44e schema:location Berlin, Heidelberg
49 schema:name Springer Berlin Heidelberg
50 rdf:type schema:Organisation
51 N96d7c890684c4826888cbfea434cf08e schema:isbn 978-3-540-61511-8
52 978-3-540-68687-3
53 schema:name Automated Deduction — Cade-13
54 rdf:type schema:Book
55 N9f8bdfb6799a47fb9e5b41a577785e57 rdf:first N39faf7aff99c4ef6a6331fdffa0970da
56 rdf:rest Ne9020dad820946e189529e2fa101a9a9
57 Na59f1b2d7ecb4fb0890203015698cb1f rdf:first sg:person.012116677555.81
58 rdf:rest rdf:nil
59 Ne9020dad820946e189529e2fa101a9a9 rdf:first N4099b164e60b4a98a15539b0fa20ee67
60 rdf:rest rdf:nil
61 Nebb5d9a03b3341549d75e474ab3bf2bf schema:name Institut für Informatik, Universität München, Oettingenstr. 67, D-80538 München
62 rdf:type schema:Organization
63 Nf5a38208090f45709821ede2a7725a9c schema:name Institut für Informatik, Universität München, Oettingenstr. 67, D-80538 München
64 rdf:type schema:Organization
65 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
66 schema:name Mathematical Sciences
67 rdf:type schema:DefinedTerm
68 anzsrc-for:0103 schema:inDefinedTermSet anzsrc-for:
69 schema:name Numerical and Computational Mathematics
70 rdf:type schema:DefinedTerm
71 sg:person.012116677555.81 schema:affiliation Nf5a38208090f45709821ede2a7725a9c
72 schema:familyName Geisler
73 schema:givenName Tim
74 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012116677555.81
75 rdf:type schema:Person
76 sg:person.07726356155.42 schema:affiliation Nebb5d9a03b3341549d75e474ab3bf2bf
77 schema:familyName Schütz
78 schema:givenName Heribert
79 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07726356155.42
80 rdf:type schema:Person
81 sg:pub.10.1007/bf00297245 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034625725
82 https://doi.org/10.1007/bf00297245
83 rdf:type schema:CreativeWork
84 https://doi.org/10.1016/0004-3702(82)90020-0 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013363801
85 rdf:type schema:CreativeWork
 




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


...