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 Nc3dc0c618e6b44baa878b200c50e9b50
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 N26451afeff70440a8ea5ad37df318965
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N1377bf4f6f9e44248feae2241b96fe38
12 schema:name Model generation with existentially quantified variables and constraints
13 schema:pagination 256-272
14 schema:productId N75317c0954f74ee4b2627fc64a98cab9
15 Nd8772a40c7be4222bf13bddc8e0f3dc4
16 Nf75ea25feadd47e9b1976f6454284b07
17 schema:publisher N68595434c70a42eabdafdffe6f4cb50f
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 N90c4861fa88e4bf085aea64a34ccf6ec
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 N1377bf4f6f9e44248feae2241b96fe38 schema:isbn 978-3-540-63459-1
28 978-3-540-69555-4
29 schema:name Algebraic and Logic Programming
30 rdf:type schema:Book
31 N26451afeff70440a8ea5ad37df318965 rdf:first Nbb0498d9cbdf48a888a9b7e8eeeb2de6
32 rdf:rest Nc13806ce6fb849fb9f193d28f7b4d1c2
33 N4af75af2fb994a3cad6d8ef3fc9cbbc6 rdf:first sg:person.07726356155.42
34 rdf:rest rdf:nil
35 N5823708b2dab4bb7b8b7498c6ab050de schema:name Institut für Informatik, Universität München, Oettingenstr. 67, D-80538 München
36 rdf:type schema:Organization
37 N64e3aba5e1d748dfb77041deed8a3e06 schema:name Institut für Informatik, Universität München, Oettingenstr. 67, D-80538 München
38 rdf:type schema:Organization
39 N68595434c70a42eabdafdffe6f4cb50f schema:location Berlin, Heidelberg
40 schema:name Springer Berlin Heidelberg
41 rdf:type schema:Organisation
42 N75317c0954f74ee4b2627fc64a98cab9 schema:name dimensions_id
43 schema:value pub.1005743991
44 rdf:type schema:PropertyValue
45 N8f138046e5314bf7b31fb00ad8dfa769 schema:familyName Meinke
46 schema:givenName Karl
47 rdf:type schema:Person
48 N90c4861fa88e4bf085aea64a34ccf6ec schema:name Springer Nature - SN SciGraph project
49 rdf:type schema:Organization
50 Nad7413fcb1f14225bc53472e6070be0c schema:familyName Heering
51 schema:givenName Jan
52 rdf:type schema:Person
53 Nbb0498d9cbdf48a888a9b7e8eeeb2de6 schema:familyName Hanus
54 schema:givenName Michael
55 rdf:type schema:Person
56 Nc13806ce6fb849fb9f193d28f7b4d1c2 rdf:first Nad7413fcb1f14225bc53472e6070be0c
57 rdf:rest Nc7c4740cbc1f4587a62d536cbec84a51
58 Nc3dc0c618e6b44baa878b200c50e9b50 rdf:first sg:person.010445445574.13
59 rdf:rest N4af75af2fb994a3cad6d8ef3fc9cbbc6
60 Nc7c4740cbc1f4587a62d536cbec84a51 rdf:first N8f138046e5314bf7b31fb00ad8dfa769
61 rdf:rest rdf:nil
62 Nd8772a40c7be4222bf13bddc8e0f3dc4 schema:name doi
63 schema:value 10.1007/bfb0027015
64 rdf:type schema:PropertyValue
65 Nf75ea25feadd47e9b1976f6454284b07 schema:name readcube_id
66 schema:value 1b5dee4a5a15b6c41a4bc4fd9cffce86e9f02930285164e09ff43688cffbbe0f
67 rdf:type schema:PropertyValue
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 N64e3aba5e1d748dfb77041deed8a3e06
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 N5823708b2dab4bb7b8b7498c6ab050de
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)


...