Efficient model generation through compilation View Full Text


Ontology type: schema:Chapter     


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

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/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/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Oettingenstr. 67, D-80538, M\u00fcnchen", 
          "id": "http://www.grid.ac/institutes/grid.5252.0", 
          "name": [
            "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Oettingenstr. 67, D-80538, M\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": {
          "alternateName": "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Oettingenstr. 67, D-80538, M\u00fcnchen", 
          "id": "http://www.grid.ac/institutes/grid.5252.0", 
          "name": [
            "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Oettingenstr. 67, D-80538, M\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"
      }
    ], 
    "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": false, 
    "isPartOf": {
      "isbn": [
        "978-3-540-61511-8", 
        "978-3-540-68687-3"
      ], 
      "name": "Automated Deduction \u2014 Cade-13", 
      "type": "Book"
    }, 
    "keywords": [
      "breadth-first search strategy", 
      "efficient model generation", 
      "TPTP problem library", 
      "theorem provers", 
      "na\u00efve implementation", 
      "search space", 
      "efficient implementation", 
      "problem library", 
      "class of problems", 
      "model generation", 
      "redundant work", 
      "Prolog programs", 
      "implementation", 
      "search strategy", 
      "central idea", 
      "SETHEO", 
      "provers", 
      "first order theory", 
      "powerful technique", 
      "benchmarks", 
      "SATCHMO", 
      "technique", 
      "fair selection", 
      "efficient strategy", 
      "library", 
      "compilation", 
      "collection", 
      "idea", 
      "space", 
      "efficiency", 
      "selection", 
      "strategies", 
      "clauses", 
      "work", 
      "method", 
      "model", 
      "class", 
      "generation", 
      "program", 
      "order theory", 
      "combination", 
      "theory", 
      "splitting", 
      "otters", 
      "problem", 
      "model-generation theorem provers", 
      "clausal first order theory", 
      "procedural Prolog program", 
      "complement splitting", 
      "theorem provers MGTP/G", 
      "provers MGTP/G", 
      "MGTP/G", 
      "range-restricted problems"
    ], 
    "name": "Efficient model generation through compilation", 
    "pagination": "433-447", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1052848223"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/3-540-61511-3_105"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/3-540-61511-3_105", 
      "https://app.dimensions.ai/details/publication/pub.1052848223"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:12", 
    "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/chapter/chapter_49.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/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.

125 TRIPLES      23 PREDICATES      79 URIs      72 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/3-540-61511-3_105 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Na7ad8bd224464341909e83e4e82d1132
4 schema:datePublished 1996
5 schema:datePublishedReg 1996-01-01
6 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”.
7 schema:editor N49dc78f2ef824109957bc630e41579a7
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Ncbad482f53234bffa8ab5c70346369c9
12 schema:keywords MGTP/G
13 Prolog programs
14 SATCHMO
15 SETHEO
16 TPTP problem library
17 benchmarks
18 breadth-first search strategy
19 central idea
20 class
21 class of problems
22 clausal first order theory
23 clauses
24 collection
25 combination
26 compilation
27 complement splitting
28 efficiency
29 efficient implementation
30 efficient model generation
31 efficient strategy
32 fair selection
33 first order theory
34 generation
35 idea
36 implementation
37 library
38 method
39 model
40 model generation
41 model-generation theorem provers
42 naïve implementation
43 order theory
44 otters
45 powerful technique
46 problem
47 problem library
48 procedural Prolog program
49 program
50 provers
51 provers MGTP/G
52 range-restricted problems
53 redundant work
54 search space
55 search strategy
56 selection
57 space
58 splitting
59 strategies
60 technique
61 theorem provers
62 theorem provers MGTP/G
63 theory
64 work
65 schema:name Efficient model generation through compilation
66 schema:pagination 433-447
67 schema:productId N3d270adb7ad84bbb847a9f0a4a0845e0
68 N62cc34d79b4d4107b6f3ffb3b0b5408d
69 schema:publisher Nf7d3c3d5f11d4615bcafecd781cf7edc
70 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052848223
71 https://doi.org/10.1007/3-540-61511-3_105
72 schema:sdDatePublished 2021-12-01T20:12
73 schema:sdLicense https://scigraph.springernature.com/explorer/license/
74 schema:sdPublisher N496debb4f20547758e2f921e1b01189d
75 schema:url https://doi.org/10.1007/3-540-61511-3_105
76 sgo:license sg:explorer/license/
77 sgo:sdDataset chapters
78 rdf:type schema:Chapter
79 N0aa22f6da9f44e9186ca84eeede1369e rdf:first Ne312802a91fa469eb7ff2a3f08b14a00
80 rdf:rest rdf:nil
81 N3d270adb7ad84bbb847a9f0a4a0845e0 schema:name doi
82 schema:value 10.1007/3-540-61511-3_105
83 rdf:type schema:PropertyValue
84 N496debb4f20547758e2f921e1b01189d schema:name Springer Nature - SN SciGraph project
85 rdf:type schema:Organization
86 N49dc78f2ef824109957bc630e41579a7 rdf:first Na0bad0fe0e394f03b6d1e65a1ee7a73c
87 rdf:rest N0aa22f6da9f44e9186ca84eeede1369e
88 N62cc34d79b4d4107b6f3ffb3b0b5408d schema:name dimensions_id
89 schema:value pub.1052848223
90 rdf:type schema:PropertyValue
91 N9c3acadc30014900aa652bd2ab5ee844 rdf:first sg:person.012116677555.81
92 rdf:rest rdf:nil
93 Na0bad0fe0e394f03b6d1e65a1ee7a73c schema:familyName McRobbie
94 schema:givenName M. A.
95 rdf:type schema:Person
96 Na7ad8bd224464341909e83e4e82d1132 rdf:first sg:person.07726356155.42
97 rdf:rest N9c3acadc30014900aa652bd2ab5ee844
98 Ncbad482f53234bffa8ab5c70346369c9 schema:isbn 978-3-540-61511-8
99 978-3-540-68687-3
100 schema:name Automated Deduction — Cade-13
101 rdf:type schema:Book
102 Ne312802a91fa469eb7ff2a3f08b14a00 schema:familyName Slaney
103 schema:givenName J. K.
104 rdf:type schema:Person
105 Nf7d3c3d5f11d4615bcafecd781cf7edc schema:name Springer Nature
106 rdf:type schema:Organisation
107 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
108 schema:name Information and Computing Sciences
109 rdf:type schema:DefinedTerm
110 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
111 schema:name Computation Theory and Mathematics
112 rdf:type schema:DefinedTerm
113 sg:person.012116677555.81 schema:affiliation grid-institutes:grid.5252.0
114 schema:familyName Geisler
115 schema:givenName Tim
116 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012116677555.81
117 rdf:type schema:Person
118 sg:person.07726356155.42 schema:affiliation grid-institutes:grid.5252.0
119 schema:familyName Schütz
120 schema:givenName Heribert
121 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07726356155.42
122 rdf:type schema:Person
123 grid-institutes:grid.5252.0 schema:alternateName Institut für Informatik, Universität München, Oettingenstr. 67, D-80538, München
124 schema:name Institut für Informatik, Universität München, Oettingenstr. 67, D-80538, München
125 rdf:type schema:Organization
 




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


...