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/2004", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Linguistics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/20", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Language, Communication and Culture", 
            "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, 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": "Ludwig Maximilian University of Munich", 
              "id": "https://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": "Ludwig Maximilian University of Munich", 
              "id": "https://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.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-58156-1_63", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007348664", 
              "https://doi.org/10.1007/3-540-58156-1_63"
            ], 
            "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-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/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": "https://doi.org/10.1016/0304-3975(94)90208-9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1040240076"
            ], 
            "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-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": "https://doi.org/10.1093/logcom/6.2.173", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059875736"
            ], 
            "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": "research_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", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "18"
          }
        ], 
        "name": "Satchmo - The Compiling and Functional Variants", 
        "pagination": "227-236", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "1bb04d3b98dfa03944e73ba3328790a385dc91ae41bd89bc6c8fe9e18e3a4aa5"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1023/a:1005851801356"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1005812032"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1023/a:1005851801356", 
          "https://app.dimensions.ai/details/publication/pub.1005812032"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-10T23:18", 
        "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_8693_00000486.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "http://link.springer.com/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.

    113 TRIPLES      21 PREDICATES      37 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1023/a:1005851801356 schema:about anzsrc-for:20
    2 anzsrc-for:2004
    3 schema:author N3ae3947010ed4e799fbd2f9721e08e34
    4 schema:citation sg:pub.10.1007/3-540-58156-1_18
    5 sg:pub.10.1007/3-540-58156-1_59
    6 sg:pub.10.1007/3-540-58156-1_63
    7 sg:pub.10.1007/3-540-61208-4_10
    8 sg:pub.10.1007/3-540-61511-3_105
    9 sg:pub.10.1007/bf00881861
    10 sg:pub.10.1007/bfb0012847
    11 sg:pub.10.1023/a:1005858625038
    12 https://doi.org/10.1016/0304-3975(94)90208-9
    13 https://doi.org/10.1093/logcom/6.2.173
    14 schema:datePublished 1997-04
    15 schema:datePublishedReg 1997-04-01
    16 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.
    17 schema:genre research_article
    18 schema:inLanguage en
    19 schema:isAccessibleForFree false
    20 schema:isPartOf N59ae8b78550f4075a1d9a86ad9475a51
    21 Nee5d8a6b409d42418c49d0e1fa1ae303
    22 sg:journal.1136522
    23 schema:name Satchmo - The Compiling and Functional Variants
    24 schema:pagination 227-236
    25 schema:productId N22cd3367702f4f80a6b3a9646206673d
    26 N24fd7c2615b5474facb14f01799455fa
    27 N926c65dd76814642b84d2f58163ee71b
    28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005812032
    29 https://doi.org/10.1023/a:1005851801356
    30 schema:sdDatePublished 2019-04-10T23:18
    31 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    32 schema:sdPublisher Nce05e8f449a74c7e8ea37ee8faee04bd
    33 schema:url http://link.springer.com/10.1023/A:1005851801356
    34 sgo:license sg:explorer/license/
    35 sgo:sdDataset articles
    36 rdf:type schema:ScholarlyArticle
    37 N1cec4c2af0f945aaade7ffb14be74f4f rdf:first sg:person.07420520067.74
    38 rdf:rest Nb219e380c2fe44d198101db2a89cd01d
    39 N22cd3367702f4f80a6b3a9646206673d schema:name readcube_id
    40 schema:value 1bb04d3b98dfa03944e73ba3328790a385dc91ae41bd89bc6c8fe9e18e3a4aa5
    41 rdf:type schema:PropertyValue
    42 N24fd7c2615b5474facb14f01799455fa schema:name doi
    43 schema:value 10.1023/a:1005851801356
    44 rdf:type schema:PropertyValue
    45 N3ae3947010ed4e799fbd2f9721e08e34 rdf:first sg:person.012116677555.81
    46 rdf:rest N1cec4c2af0f945aaade7ffb14be74f4f
    47 N59ae8b78550f4075a1d9a86ad9475a51 schema:volumeNumber 18
    48 rdf:type schema:PublicationVolume
    49 N926c65dd76814642b84d2f58163ee71b schema:name dimensions_id
    50 schema:value pub.1005812032
    51 rdf:type schema:PropertyValue
    52 Nb219e380c2fe44d198101db2a89cd01d rdf:first sg:person.07726356155.42
    53 rdf:rest rdf:nil
    54 Nce05e8f449a74c7e8ea37ee8faee04bd schema:name Springer Nature - SN SciGraph project
    55 rdf:type schema:Organization
    56 Nee5d8a6b409d42418c49d0e1fa1ae303 schema:issueNumber 2
    57 rdf:type schema:PublicationIssue
    58 anzsrc-for:20 schema:inDefinedTermSet anzsrc-for:
    59 schema:name Language, Communication and Culture
    60 rdf:type schema:DefinedTerm
    61 anzsrc-for:2004 schema:inDefinedTermSet anzsrc-for:
    62 schema:name Linguistics
    63 rdf:type schema:DefinedTerm
    64 sg:journal.1136522 schema:issn 0168-7433
    65 1573-0670
    66 schema:name Journal of Automated Reasoning
    67 rdf:type schema:Periodical
    68 sg:person.012116677555.81 schema:affiliation https://www.grid.ac/institutes/grid.5252.0
    69 schema:familyName Geisler
    70 schema:givenName Tim
    71 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012116677555.81
    72 rdf:type schema:Person
    73 sg:person.07420520067.74 schema:affiliation https://www.grid.ac/institutes/grid.5252.0
    74 schema:familyName Panne
    75 schema:givenName Sven
    76 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07420520067.74
    77 rdf:type schema:Person
    78 sg:person.07726356155.42 schema:affiliation https://www.grid.ac/institutes/grid.5252.0
    79 schema:familyName Schütz
    80 schema:givenName Heribert
    81 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07726356155.42
    82 rdf:type schema:Person
    83 sg:pub.10.1007/3-540-58156-1_18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1015009827
    84 https://doi.org/10.1007/3-540-58156-1_18
    85 rdf:type schema:CreativeWork
    86 sg:pub.10.1007/3-540-58156-1_59 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042701875
    87 https://doi.org/10.1007/3-540-58156-1_59
    88 rdf:type schema:CreativeWork
    89 sg:pub.10.1007/3-540-58156-1_63 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007348664
    90 https://doi.org/10.1007/3-540-58156-1_63
    91 rdf:type schema:CreativeWork
    92 sg:pub.10.1007/3-540-61208-4_10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018594473
    93 https://doi.org/10.1007/3-540-61208-4_10
    94 rdf:type schema:CreativeWork
    95 sg:pub.10.1007/3-540-61511-3_105 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052848223
    96 https://doi.org/10.1007/3-540-61511-3_105
    97 rdf:type schema:CreativeWork
    98 sg:pub.10.1007/bf00881861 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023028400
    99 https://doi.org/10.1007/bf00881861
    100 rdf:type schema:CreativeWork
    101 sg:pub.10.1007/bfb0012847 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031681210
    102 https://doi.org/10.1007/bfb0012847
    103 rdf:type schema:CreativeWork
    104 sg:pub.10.1023/a:1005858625038 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001925182
    105 https://doi.org/10.1023/a:1005858625038
    106 rdf:type schema:CreativeWork
    107 https://doi.org/10.1016/0304-3975(94)90208-9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1040240076
    108 rdf:type schema:CreativeWork
    109 https://doi.org/10.1093/logcom/6.2.173 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059875736
    110 rdf:type schema:CreativeWork
    111 https://www.grid.ac/institutes/grid.5252.0 schema:alternateName Ludwig Maximilian University of Munich
    112 schema:name Institut für Informatik, Universität München, München, Germany
    113 rdf:type schema:Organization
     




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


    ...