Model generation with existentially quantified variables and constraints View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

1997

AUTHORS

Slim Abdennadher , Heribert Schütz

ABSTRACT

In this paper we present the CPUHR-tableau calculus, a modification of positive unit hyperresolution (PURR) tableaux, the calculus underlying the model generator and theorem prover Satchmo. In addition to clausal first order logic, CPUHR tableaux are able to manipulate existentially quantified variables without Skolemization, and they allow to attach constraints to these variables as in constraint logic programming. This extension allows to handle efficiently many realistic model generation problems that cannot be handled by model generators for clausal theories such as PURR tableaux. In this paper we deal with CPUHR tableaux only for formulas without function symbols other than constants. More... »

PAGES

256-272

Book

TITLE

Algebraic and Logic Programming

ISBN

978-3-540-63459-1
978-3-540-69555-4

Identifiers

URI

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

DOI

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

DIMENSIONS

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


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/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }, 
      {
        "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"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "name": [
            "Institut f\u00fcr Informatik, Universit\u00e4t M\u00fcnchen, Oettingenstr. 67, D-80538\u00a0M\u00fcnchen"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Abdennadher", 
        "givenName": "Slim", 
        "id": "sg:person.010445445574.13", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010445445574.13"
        ], 
        "type": "Person"
      }, 
      {
        "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"
      }
    ], 
    "datePublished": "1997", 
    "datePublishedReg": "1997-01-01", 
    "description": "In this paper we present the CPUHR-tableau calculus, a modification of positive unit hyperresolution (PURR) tableaux, the calculus underlying the model generator and theorem prover Satchmo. In addition to clausal first order logic, CPUHR tableaux are able to manipulate existentially quantified variables without Skolemization, and they allow to attach constraints to these variables as in constraint logic programming. This extension allows to handle efficiently many realistic model generation problems that cannot be handled by model generators for clausal theories such as PURR tableaux. In this paper we deal with CPUHR tableaux only for formulas without function symbols other than constants.", 
    "editor": [
      {
        "familyName": "Hanus", 
        "givenName": "Michael", 
        "type": "Person"
      }, 
      {
        "familyName": "Heering", 
        "givenName": "Jan", 
        "type": "Person"
      }, 
      {
        "familyName": "Meinke", 
        "givenName": "Karl", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/bfb0027015", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-63459-1", 
        "978-3-540-69555-4"
      ], 
      "name": "Algebraic and Logic Programming", 
      "type": "Book"
    }, 
    "name": "Model generation with existentially quantified variables and constraints", 
    "pagination": "256-272", 
    "productId": [
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/bfb0027015"
        ]
      }, 
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "1b5dee4a5a15b6c41a4bc4fd9cffce86e9f02930285164e09ff43688cffbbe0f"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1005743991"
        ]
      }
    ], 
    "publisher": {
      "location": "Berlin, Heidelberg", 
      "name": "Springer Berlin Heidelberg", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/bfb0027015", 
      "https://app.dimensions.ai/details/publication/pub.1005743991"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2019-04-15T20:46", 
    "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_8690_00000009.jsonl", 
    "type": "Chapter", 
    "url": "http://link.springer.com/10.1007/BFb0027015"
  }
]
 

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

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

Turtle is a human-readable linked data format.

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

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

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


 

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

83 TRIPLES      22 PREDICATES      27 URIs      20 LITERALS      8 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/bfb0027015 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N37eb3880f2d04d448db87dbe34e1f763
4 schema:datePublished 1997
5 schema:datePublishedReg 1997-01-01
6 schema:description In this paper we present the CPUHR-tableau calculus, a modification of positive unit hyperresolution (PURR) tableaux, the calculus underlying the model generator and theorem prover Satchmo. In addition to clausal first order logic, CPUHR tableaux are able to manipulate existentially quantified variables without Skolemization, and they allow to attach constraints to these variables as in constraint logic programming. This extension allows to handle efficiently many realistic model generation problems that cannot be handled by model generators for clausal theories such as PURR tableaux. In this paper we deal with CPUHR tableaux only for formulas without function symbols other than constants.
7 schema:editor N49d2d05873514d12bba6f47df44dccd7
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf Nd600570a9753451cbd4faea55c15c14a
12 schema:name Model generation with existentially quantified variables and constraints
13 schema:pagination 256-272
14 schema:productId N166766d33a164da68f0f786d0d5e45d4
15 Na8e276585cf744c7abac581b03ecadf7
16 Nbdd9d2caa1534bff80bd762a30b5edf9
17 schema:publisher N81231b3336eb44638c37bf22d4a881c9
18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005743991
19 https://doi.org/10.1007/bfb0027015
20 schema:sdDatePublished 2019-04-15T20:46
21 schema:sdLicense https://scigraph.springernature.com/explorer/license/
22 schema:sdPublisher Na5a0bd11894b4dc5b842412aa6a3f980
23 schema:url http://link.springer.com/10.1007/BFb0027015
24 sgo:license sg:explorer/license/
25 sgo:sdDataset chapters
26 rdf:type schema:Chapter
27 N14000c034ebd4b1e87f46d7191875855 schema:familyName Meinke
28 schema:givenName Karl
29 rdf:type schema:Person
30 N166766d33a164da68f0f786d0d5e45d4 schema:name dimensions_id
31 schema:value pub.1005743991
32 rdf:type schema:PropertyValue
33 N1c7aa314e23a4cdc980a552f9efe2361 rdf:first sg:person.07726356155.42
34 rdf:rest rdf:nil
35 N37eb3880f2d04d448db87dbe34e1f763 rdf:first sg:person.010445445574.13
36 rdf:rest N1c7aa314e23a4cdc980a552f9efe2361
37 N49d2d05873514d12bba6f47df44dccd7 rdf:first N5707ff50417241c888166f50c2fe0f7d
38 rdf:rest Nd0f8c3db3d8942908ca7b1f4f20454be
39 N5707ff50417241c888166f50c2fe0f7d schema:familyName Hanus
40 schema:givenName Michael
41 rdf:type schema:Person
42 N687d5c88034443e1813abcd3f5212f8f schema:name Institut für Informatik, Universität München, Oettingenstr. 67, D-80538 München
43 rdf:type schema:Organization
44 N81231b3336eb44638c37bf22d4a881c9 schema:location Berlin, Heidelberg
45 schema:name Springer Berlin Heidelberg
46 rdf:type schema:Organisation
47 Na5a0bd11894b4dc5b842412aa6a3f980 schema:name Springer Nature - SN SciGraph project
48 rdf:type schema:Organization
49 Na8e276585cf744c7abac581b03ecadf7 schema:name doi
50 schema:value 10.1007/bfb0027015
51 rdf:type schema:PropertyValue
52 Nbdd9d2caa1534bff80bd762a30b5edf9 schema:name readcube_id
53 schema:value 1b5dee4a5a15b6c41a4bc4fd9cffce86e9f02930285164e09ff43688cffbbe0f
54 rdf:type schema:PropertyValue
55 Nbef03dd9548344fb934c3fe125683ccf schema:name Institut für Informatik, Universität München, Oettingenstr. 67, D-80538 München
56 rdf:type schema:Organization
57 Nd0f8c3db3d8942908ca7b1f4f20454be rdf:first Nf4be4adb720847919f3ce21c23a1d233
58 rdf:rest Nfc63a70df8eb4de79a613206ae8dabc4
59 Nd600570a9753451cbd4faea55c15c14a schema:isbn 978-3-540-63459-1
60 978-3-540-69555-4
61 schema:name Algebraic and Logic Programming
62 rdf:type schema:Book
63 Nf4be4adb720847919f3ce21c23a1d233 schema:familyName Heering
64 schema:givenName Jan
65 rdf:type schema:Person
66 Nfc63a70df8eb4de79a613206ae8dabc4 rdf:first N14000c034ebd4b1e87f46d7191875855
67 rdf:rest rdf:nil
68 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
69 schema:name Information and Computing Sciences
70 rdf:type schema:DefinedTerm
71 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
72 schema:name Computer Software
73 rdf:type schema:DefinedTerm
74 sg:person.010445445574.13 schema:affiliation N687d5c88034443e1813abcd3f5212f8f
75 schema:familyName Abdennadher
76 schema:givenName Slim
77 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010445445574.13
78 rdf:type schema:Person
79 sg:person.07726356155.42 schema:affiliation Nbef03dd9548344fb934c3fe125683ccf
80 schema:familyName Schütz
81 schema:givenName Heribert
82 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07726356155.42
83 rdf:type schema:Person
 




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


...