Satchmo - The Compiling and Functional Variants View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1997-04

AUTHORS

Tim Geisler, Sven Panne, Heribert Schütz

ABSTRACT

Compiling Satchmo and Functional Satchmo are two variants of the model generator Satchmo, incorporating enhancements in different directions. Compiling Satchmo is based on the observation that Satchmo (like any model generator or theorem prover) can be seen as an interpreter for a program given as a logical theory, and that this interpretation layer can be avoided by compilation of the theory into a directly executable program. Functional Satchmo is an implementation of Satchmo's calculus in a purely functional language supporting lazy evaluation. More... »

PAGES

227-236

References to SciGraph publications

  • 1996. Minimal model generation with positive unit hyper-resolution tableaux in THEOREM PROVING WITH ANALYTIC TABLEAUX AND RELATED METHODS
  • 1996. Efficient model generation through compilation in AUTOMATED DEDUCTION — CADE-13
  • 1995-06. SATCHMORE: SATCHMO with RElevancy in JOURNAL OF AUTOMATED REASONING
  • 1994. The TPTP problem library in AUTOMATED DEDUCTION — CADE-12
  • 1988. SATCHMO: A theorem prover implemented in Prolog in 9TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
  • 1994. FINDER: Finite domain enumerator system description in AUTOMATED DEDUCTION — CADE-12
  • 1994. SETHEO V3.2: Recent developments in AUTOMATED DEDUCTION — CADE-12
  • 1997-04. The Procedures of the CADE-13 ATP System Competition in JOURNAL OF AUTOMATED REASONING
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1023/a:1005851801356

    DOI

    http://dx.doi.org/10.1023/a:1005851801356

    DIMENSIONS

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


    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/17", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Psychology and Cognitive 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"
          }, 
          {
            "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"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/1702", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Cognitive Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany", 
              "id": "http://www.grid.ac/institutes/grid.5252.0", 
              "name": [
                "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"
              ], 
              "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"
          }, 
          {
            "affiliation": {
              "alternateName": "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany", 
              "id": "http://www.grid.ac/institutes/grid.5252.0", 
              "name": [
                "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Panne", 
            "givenName": "Sven", 
            "id": "sg:person.07420520067.74", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07420520067.74"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany", 
              "id": "http://www.grid.ac/institutes/grid.5252.0", 
              "name": [
                "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, 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": "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/bfb0012847", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1031681210", 
              "https://doi.org/10.1007/bfb0012847"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1023/a:1005858625038", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1001925182", 
              "https://doi.org/10.1023/a:1005858625038"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-61511-3_105", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1052848223", 
              "https://doi.org/10.1007/3-540-61511-3_105"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-58156-1_18", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1015009827", 
              "https://doi.org/10.1007/3-540-58156-1_18"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-58156-1_59", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1042701875", 
              "https://doi.org/10.1007/3-540-58156-1_59"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-61208-4_10", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018594473", 
              "https://doi.org/10.1007/3-540-61208-4_10"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-58156-1_63", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007348664", 
              "https://doi.org/10.1007/3-540-58156-1_63"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1997-04", 
        "datePublishedReg": "1997-04-01", 
        "description": "Compiling Satchmo and Functional Satchmo are two variants of the model generator Satchmo, incorporating enhancements in different directions. Compiling Satchmo is based on the observation that Satchmo (like any model generator or theorem prover) can be seen as an interpreter for a program given as a logical theory, and that this interpretation layer can be avoided by compilation of the theory into a directly executable program. Functional Satchmo is an implementation of Satchmo's calculus in a purely functional language supporting lazy evaluation.", 
        "genre": "article", 
        "id": "sg:pub.10.1023/a:1005851801356", 
        "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": "18"
          }
        ], 
        "keywords": [
          "variants", 
          "logical theory", 
          "theory", 
          "calculus", 
          "functional variants", 
          "SATCHMO", 
          "enhancement", 
          "different directions", 
          "observations", 
          "interpreters", 
          "program", 
          "executable program", 
          "implementation", 
          "functional language", 
          "language", 
          "lazy evaluation", 
          "evaluation", 
          "compiling", 
          "direction", 
          "layer", 
          "compilation", 
          "Compiling Satchmo", 
          "Functional Satchmo", 
          "model generator Satchmo", 
          "generator Satchmo", 
          "interpretation layer", 
          "Satchmo's calculus"
        ], 
        "name": "Satchmo - The Compiling and Functional Variants", 
        "pagination": "227-236", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1005812032"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1023/a:1005851801356"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1023/a:1005851801356", 
          "https://app.dimensions.ai/details/publication/pub.1005812032"
        ], 
        "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_285.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1023/a:1005851801356"
      }
    ]
     

    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.1023/a:1005851801356'

    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.1023/a:1005851801356'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1023/a:1005851801356'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1023/a:1005851801356'


     

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

    143 TRIPLES      22 PREDICATES      64 URIs      45 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1023/a:1005851801356 schema:about anzsrc-for:08
    2 anzsrc-for:0801
    3 anzsrc-for:0802
    4 anzsrc-for:17
    5 anzsrc-for:1702
    6 schema:author N5f75fa90b9224c0193be125263870056
    7 schema:citation sg:pub.10.1007/3-540-58156-1_18
    8 sg:pub.10.1007/3-540-58156-1_59
    9 sg:pub.10.1007/3-540-58156-1_63
    10 sg:pub.10.1007/3-540-61208-4_10
    11 sg:pub.10.1007/3-540-61511-3_105
    12 sg:pub.10.1007/bf00881861
    13 sg:pub.10.1007/bfb0012847
    14 sg:pub.10.1023/a:1005858625038
    15 schema:datePublished 1997-04
    16 schema:datePublishedReg 1997-04-01
    17 schema:description Compiling Satchmo and Functional Satchmo are two variants of the model generator Satchmo, incorporating enhancements in different directions. Compiling Satchmo is based on the observation that Satchmo (like any model generator or theorem prover) can be seen as an interpreter for a program given as a logical theory, and that this interpretation layer can be avoided by compilation of the theory into a directly executable program. Functional Satchmo is an implementation of Satchmo's calculus in a purely functional language supporting lazy evaluation.
    18 schema:genre article
    19 schema:inLanguage en
    20 schema:isAccessibleForFree false
    21 schema:isPartOf N070cf4201cdb4568acb2f2dfbe99ebcb
    22 N1c21b6d20f1a49419588aee2e885530b
    23 sg:journal.1136522
    24 schema:keywords Compiling Satchmo
    25 Functional Satchmo
    26 SATCHMO
    27 Satchmo's calculus
    28 calculus
    29 compilation
    30 compiling
    31 different directions
    32 direction
    33 enhancement
    34 evaluation
    35 executable program
    36 functional language
    37 functional variants
    38 generator Satchmo
    39 implementation
    40 interpretation layer
    41 interpreters
    42 language
    43 layer
    44 lazy evaluation
    45 logical theory
    46 model generator Satchmo
    47 observations
    48 program
    49 theory
    50 variants
    51 schema:name Satchmo - The Compiling and Functional Variants
    52 schema:pagination 227-236
    53 schema:productId N29bb50aa62014a1c94cf8c692abba7c4
    54 N9ee09a18080240308af4990f96213f7e
    55 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005812032
    56 https://doi.org/10.1023/a:1005851801356
    57 schema:sdDatePublished 2021-12-01T19:10
    58 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    59 schema:sdPublisher N1b80f45f034c4e1bb8119dd7190c91d6
    60 schema:url https://doi.org/10.1023/a:1005851801356
    61 sgo:license sg:explorer/license/
    62 sgo:sdDataset articles
    63 rdf:type schema:ScholarlyArticle
    64 N070cf4201cdb4568acb2f2dfbe99ebcb schema:issueNumber 2
    65 rdf:type schema:PublicationIssue
    66 N1b80f45f034c4e1bb8119dd7190c91d6 schema:name Springer Nature - SN SciGraph project
    67 rdf:type schema:Organization
    68 N1c21b6d20f1a49419588aee2e885530b schema:volumeNumber 18
    69 rdf:type schema:PublicationVolume
    70 N29bb50aa62014a1c94cf8c692abba7c4 schema:name doi
    71 schema:value 10.1023/a:1005851801356
    72 rdf:type schema:PropertyValue
    73 N5f75fa90b9224c0193be125263870056 rdf:first sg:person.012116677555.81
    74 rdf:rest N8cd36d958bb24c62a51cac64ecf7f09f
    75 N8b62a968fcb545bab0d767d63b8eb26d rdf:first sg:person.07726356155.42
    76 rdf:rest rdf:nil
    77 N8cd36d958bb24c62a51cac64ecf7f09f rdf:first sg:person.07420520067.74
    78 rdf:rest N8b62a968fcb545bab0d767d63b8eb26d
    79 N9ee09a18080240308af4990f96213f7e schema:name dimensions_id
    80 schema:value pub.1005812032
    81 rdf:type schema:PropertyValue
    82 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    83 schema:name Information and Computing Sciences
    84 rdf:type schema:DefinedTerm
    85 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
    86 schema:name Artificial Intelligence and Image Processing
    87 rdf:type schema:DefinedTerm
    88 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    89 schema:name Computation Theory and Mathematics
    90 rdf:type schema:DefinedTerm
    91 anzsrc-for:17 schema:inDefinedTermSet anzsrc-for:
    92 schema:name Psychology and Cognitive Sciences
    93 rdf:type schema:DefinedTerm
    94 anzsrc-for:1702 schema:inDefinedTermSet anzsrc-for:
    95 schema:name Cognitive Sciences
    96 rdf:type schema:DefinedTerm
    97 sg:journal.1136522 schema:issn 0168-7433
    98 1573-0670
    99 schema:name Journal of Automated Reasoning
    100 schema:publisher Springer Nature
    101 rdf:type schema:Periodical
    102 sg:person.012116677555.81 schema:affiliation grid-institutes:grid.5252.0
    103 schema:familyName Geisler
    104 schema:givenName Tim
    105 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012116677555.81
    106 rdf:type schema:Person
    107 sg:person.07420520067.74 schema:affiliation grid-institutes:grid.5252.0
    108 schema:familyName Panne
    109 schema:givenName Sven
    110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07420520067.74
    111 rdf:type schema:Person
    112 sg:person.07726356155.42 schema:affiliation grid-institutes:grid.5252.0
    113 schema:familyName Schütz
    114 schema:givenName Heribert
    115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07726356155.42
    116 rdf:type schema:Person
    117 sg:pub.10.1007/3-540-58156-1_18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1015009827
    118 https://doi.org/10.1007/3-540-58156-1_18
    119 rdf:type schema:CreativeWork
    120 sg:pub.10.1007/3-540-58156-1_59 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042701875
    121 https://doi.org/10.1007/3-540-58156-1_59
    122 rdf:type schema:CreativeWork
    123 sg:pub.10.1007/3-540-58156-1_63 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007348664
    124 https://doi.org/10.1007/3-540-58156-1_63
    125 rdf:type schema:CreativeWork
    126 sg:pub.10.1007/3-540-61208-4_10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018594473
    127 https://doi.org/10.1007/3-540-61208-4_10
    128 rdf:type schema:CreativeWork
    129 sg:pub.10.1007/3-540-61511-3_105 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052848223
    130 https://doi.org/10.1007/3-540-61511-3_105
    131 rdf:type schema:CreativeWork
    132 sg:pub.10.1007/bf00881861 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023028400
    133 https://doi.org/10.1007/bf00881861
    134 rdf:type schema:CreativeWork
    135 sg:pub.10.1007/bfb0012847 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031681210
    136 https://doi.org/10.1007/bfb0012847
    137 rdf:type schema:CreativeWork
    138 sg:pub.10.1023/a:1005858625038 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001925182
    139 https://doi.org/10.1023/a:1005858625038
    140 rdf:type schema:CreativeWork
    141 grid-institutes:grid.5252.0 schema:alternateName Institut für Informatik, Universität München, München, Germany
    142 schema:name Institut für Informatik, Universität München, München, Germany
    143 rdf:type schema:Organization
     




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


    ...