SATCHMO: A theorem prover implemented in Prolog View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

1988

AUTHORS

Rainer Manthey , François Bry

ABSTRACT

Satchmo is a theorem prover consisting of just a few short and simple Prolog programs. Prolog may be used for representing problem clauses as well. SATCHMO is based on a model-generation paradigm. It is refutation-complete if used in a level-saturation manner. The paper provides a thorough report on experiences with SATCHMO. A considerable amount of problems could be solved with surprising efficiency. More... »

PAGES

415-434

Book

TITLE

9th International Conference on Automated Deduction

ISBN

3-540-19343-X

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/bfb0012847

DOI

http://dx.doi.org/10.1007/bfb0012847

DIMENSIONS

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


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": "ECRC, Arabellastr. 17, D-8000, Muenchen 81, West Germany", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "ECRC, Arabellastr. 17, D-8000, Muenchen 81, West Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Manthey", 
        "givenName": "Rainer", 
        "id": "sg:person.014772664453.90", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014772664453.90"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "ECRC, Arabellastr. 17, D-8000, Muenchen 81, West Germany", 
          "id": "http://www.grid.ac/institutes/None", 
          "name": [
            "ECRC, Arabellastr. 17, D-8000, Muenchen 81, West Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Bry", 
        "givenName": "Fran\u00e7ois", 
        "id": "sg:person.013736407044.86", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013736407044.86"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "1988", 
    "datePublishedReg": "1988-01-01", 
    "description": "Satchmo is a theorem prover consisting of just a few short and simple Prolog programs. Prolog may be used for representing problem clauses as well. SATCHMO is based on a model-generation paradigm. It is refutation-complete if used in a level-saturation manner. The paper provides a thorough report on experiences with SATCHMO. A considerable amount of problems could be solved with surprising efficiency.", 
    "editor": [
      {
        "familyName": "Lusk", 
        "givenName": "Ewing", 
        "type": "Person"
      }, 
      {
        "familyName": "Overbeek", 
        "givenName": "Ross", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/bfb0012847", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "3-540-19343-X"
      ], 
      "name": "9th International Conference on Automated Deduction", 
      "type": "Book"
    }, 
    "keywords": [
      "SATCHMO", 
      "Prolog programs", 
      "Prolog", 
      "paradigm", 
      "considerable amount", 
      "surprising efficiency", 
      "theorem", 
      "program", 
      "clauses", 
      "manner", 
      "experience", 
      "amount", 
      "efficiency", 
      "paper", 
      "thorough report", 
      "report", 
      "problem", 
      "simple Prolog programs", 
      "problem clauses", 
      "model-generation paradigm", 
      "level-saturation manner"
    ], 
    "name": "SATCHMO: A theorem prover implemented in Prolog", 
    "pagination": "415-434", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1031681210"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/bfb0012847"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/bfb0012847", 
      "https://app.dimensions.ai/details/publication/pub.1031681210"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T19:56", 
    "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_126.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/bfb0012847"
  }
]
 

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/bfb0012847'

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/bfb0012847'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/bfb0012847'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/bfb0012847'


 

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

92 TRIPLES      23 PREDICATES      47 URIs      40 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/bfb0012847 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N0c20949c4e0e4e7693491281af3d1572
4 schema:datePublished 1988
5 schema:datePublishedReg 1988-01-01
6 schema:description Satchmo is a theorem prover consisting of just a few short and simple Prolog programs. Prolog may be used for representing problem clauses as well. SATCHMO is based on a model-generation paradigm. It is refutation-complete if used in a level-saturation manner. The paper provides a thorough report on experiences with SATCHMO. A considerable amount of problems could be solved with surprising efficiency.
7 schema:editor N518359b6b8e34976a145f59506c30a96
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N04647e76604e47babb589e93ebc50be0
12 schema:keywords Prolog
13 Prolog programs
14 SATCHMO
15 amount
16 clauses
17 considerable amount
18 efficiency
19 experience
20 level-saturation manner
21 manner
22 model-generation paradigm
23 paper
24 paradigm
25 problem
26 problem clauses
27 program
28 report
29 simple Prolog programs
30 surprising efficiency
31 theorem
32 thorough report
33 schema:name SATCHMO: A theorem prover implemented in Prolog
34 schema:pagination 415-434
35 schema:productId N0a07225fc76646d086a3b138b13b1485
36 Nbc42c93dd28e4ad691330d5e92b21374
37 schema:publisher N2a236911a48e403aa7f2a13a230cefd7
38 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031681210
39 https://doi.org/10.1007/bfb0012847
40 schema:sdDatePublished 2021-12-01T19:56
41 schema:sdLicense https://scigraph.springernature.com/explorer/license/
42 schema:sdPublisher Nc52d9398a93b4e38a50af14da95466c2
43 schema:url https://doi.org/10.1007/bfb0012847
44 sgo:license sg:explorer/license/
45 sgo:sdDataset chapters
46 rdf:type schema:Chapter
47 N04647e76604e47babb589e93ebc50be0 schema:isbn 3-540-19343-X
48 schema:name 9th International Conference on Automated Deduction
49 rdf:type schema:Book
50 N0a07225fc76646d086a3b138b13b1485 schema:name doi
51 schema:value 10.1007/bfb0012847
52 rdf:type schema:PropertyValue
53 N0c20949c4e0e4e7693491281af3d1572 rdf:first sg:person.014772664453.90
54 rdf:rest N7d3d0a44987240e6a4dea437bd69d8d4
55 N206a0f423ea64d88896ac9e18631d645 schema:familyName Lusk
56 schema:givenName Ewing
57 rdf:type schema:Person
58 N2a236911a48e403aa7f2a13a230cefd7 schema:name Springer Nature
59 rdf:type schema:Organisation
60 N4c5a9e0e0e9e4cecafd23d2b99a6badf rdf:first Ne6bf26362acb471ebae598cbaf6e112f
61 rdf:rest rdf:nil
62 N518359b6b8e34976a145f59506c30a96 rdf:first N206a0f423ea64d88896ac9e18631d645
63 rdf:rest N4c5a9e0e0e9e4cecafd23d2b99a6badf
64 N7d3d0a44987240e6a4dea437bd69d8d4 rdf:first sg:person.013736407044.86
65 rdf:rest rdf:nil
66 Nbc42c93dd28e4ad691330d5e92b21374 schema:name dimensions_id
67 schema:value pub.1031681210
68 rdf:type schema:PropertyValue
69 Nc52d9398a93b4e38a50af14da95466c2 schema:name Springer Nature - SN SciGraph project
70 rdf:type schema:Organization
71 Ne6bf26362acb471ebae598cbaf6e112f schema:familyName Overbeek
72 schema:givenName Ross
73 rdf:type schema:Person
74 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
75 schema:name Information and Computing Sciences
76 rdf:type schema:DefinedTerm
77 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
78 schema:name Computation Theory and Mathematics
79 rdf:type schema:DefinedTerm
80 sg:person.013736407044.86 schema:affiliation grid-institutes:None
81 schema:familyName Bry
82 schema:givenName François
83 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013736407044.86
84 rdf:type schema:Person
85 sg:person.014772664453.90 schema:affiliation grid-institutes:None
86 schema:familyName Manthey
87 schema:givenName Rainer
88 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014772664453.90
89 rdf:type schema:Person
90 grid-institutes:None schema:alternateName ECRC, Arabellastr. 17, D-8000, Muenchen 81, West Germany
91 schema:name ECRC, Arabellastr. 17, D-8000, Muenchen 81, West Germany
92 rdf:type schema:Organization
 




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


...