Proving Termination of Constraint Solver Programs View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2000

AUTHORS

Thom Frühwirth

ABSTRACT

We adapt and extend existing approaches to termination in rule-based languages (logic programming and rewriting systems) to prove termination of actually implemented CHR constraint solvers. CHR (Constraint Handling Rules) are a declarative language especially designed for writing constraint solvers. CHR are a concurrent constraint logic programming language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. The approach allows to prove termination of many constraint solvers, from Boolean and arithmetic to terminological and path-consistent constraints. Because of multi-heads, our termination orders must consider conjunctions, while atomic formulas suffice in usual approaches. Our results indicate that in practice, proving termination for concurrent constraint logic programs may not be harder than for other classes of logic programming languages, contrary to what has been feared in the literature. More... »

PAGES

298-317

References to SciGraph publications

  • 2005-06-10. Operational semantics and confluence of constraint propagation rules in PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING-CP97
  • Book

    TITLE

    New Trends in Constraints

    ISBN

    978-3-540-67885-4
    978-3-540-44654-5

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/3-540-44654-0_15

    DOI

    http://dx.doi.org/10.1007/3-540-44654-0_15

    DIMENSIONS

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


    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": {
              "alternateName": "Ludwig Maximilian University of Munich", 
              "id": "https://www.grid.ac/institutes/grid.5252.0", 
              "name": [
                "Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Oettingenstrasse 67, D-80538\u00a0Munich, Germany"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Fr\u00fchwirth", 
            "givenName": "Thom", 
            "id": "sg:person.013750414271.15", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013750414271.15"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1016/0004-3702(85)90041-4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004121645"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0004-3702(85)90041-4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004121645"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0743-1066(94)90033-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004885944"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0743-1066(93)90014-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007843535"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0017444", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010989701", 
              "https://doi.org/10.1007/bfb0017444"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0017444", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010989701", 
              "https://doi.org/10.1007/bfb0017444"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/s0747-7171(87)80022-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1026818855"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2000", 
        "datePublishedReg": "2000-01-01", 
        "description": "We adapt and extend existing approaches to termination in rule-based languages (logic programming and rewriting systems) to prove termination of actually implemented CHR constraint solvers. CHR (Constraint Handling Rules) are a declarative language especially designed for writing constraint solvers. CHR are a concurrent constraint logic programming language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. The approach allows to prove termination of many constraint solvers, from Boolean and arithmetic to terminological and path-consistent constraints. Because of multi-heads, our termination orders must consider conjunctions, while atomic formulas suffice in usual approaches. Our results indicate that in practice, proving termination for concurrent constraint logic programs may not be harder than for other classes of logic programming languages, contrary to what has been feared in the literature.", 
        "editor": [
          {
            "familyName": "Apt", 
            "givenName": "Krzysztof R.", 
            "type": "Person"
          }, 
          {
            "familyName": "Monfroy", 
            "givenName": "Eric", 
            "type": "Person"
          }, 
          {
            "familyName": "Kakas", 
            "givenName": "Antonis C.", 
            "type": "Person"
          }, 
          {
            "familyName": "Rossi", 
            "givenName": "Francesca", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/3-540-44654-0_15", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": true, 
        "isPartOf": {
          "isbn": [
            "978-3-540-67885-4", 
            "978-3-540-44654-5"
          ], 
          "name": "New Trends in Constraints", 
          "type": "Book"
        }, 
        "name": "Proving Termination of Constraint Solver Programs", 
        "pagination": "298-317", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/3-540-44654-0_15"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "d119287e2b87c75d5042dc7715c6d8c266bc6057dd18798e6e9ec71bb37ef27d"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1043896941"
            ]
          }
        ], 
        "publisher": {
          "location": "Berlin, Heidelberg", 
          "name": "Springer Berlin Heidelberg", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/3-540-44654-0_15", 
          "https://app.dimensions.ai/details/publication/pub.1043896941"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-15T17:16", 
        "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_8678_00000270.jsonl", 
        "type": "Chapter", 
        "url": "http://link.springer.com/10.1007/3-540-44654-0_15"
      }
    ]
     

    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/3-540-44654-0_15'

    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/3-540-44654-0_15'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-44654-0_15'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/3-540-44654-0_15'


     

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

    96 TRIPLES      23 PREDICATES      32 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/3-540-44654-0_15 schema:about anzsrc-for:08
    2 anzsrc-for:0803
    3 schema:author N1350b954c9774c3d959ae7acf4a7d44d
    4 schema:citation sg:pub.10.1007/bfb0017444
    5 https://doi.org/10.1016/0004-3702(85)90041-4
    6 https://doi.org/10.1016/0743-1066(93)90014-8
    7 https://doi.org/10.1016/0743-1066(94)90033-7
    8 https://doi.org/10.1016/s0747-7171(87)80022-6
    9 schema:datePublished 2000
    10 schema:datePublishedReg 2000-01-01
    11 schema:description We adapt and extend existing approaches to termination in rule-based languages (logic programming and rewriting systems) to prove termination of actually implemented CHR constraint solvers. CHR (Constraint Handling Rules) are a declarative language especially designed for writing constraint solvers. CHR are a concurrent constraint logic programming language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. The approach allows to prove termination of many constraint solvers, from Boolean and arithmetic to terminological and path-consistent constraints. Because of multi-heads, our termination orders must consider conjunctions, while atomic formulas suffice in usual approaches. Our results indicate that in practice, proving termination for concurrent constraint logic programs may not be harder than for other classes of logic programming languages, contrary to what has been feared in the literature.
    12 schema:editor N1621dabed5994928ba598ac0937e866c
    13 schema:genre chapter
    14 schema:inLanguage en
    15 schema:isAccessibleForFree true
    16 schema:isPartOf Nbef17545347f40abb464b2d68567b421
    17 schema:name Proving Termination of Constraint Solver Programs
    18 schema:pagination 298-317
    19 schema:productId N30aa3ca2d2964809b8863fe7eb409ba7
    20 N7cc8eb4b10ca4f53988b94088396f200
    21 Nb7e5c9060e48450697954c0420d98acb
    22 schema:publisher Nb14cd876d79c4774835f1dadc57562f7
    23 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043896941
    24 https://doi.org/10.1007/3-540-44654-0_15
    25 schema:sdDatePublished 2019-04-15T17:16
    26 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    27 schema:sdPublisher N11d2c7d82b364db1891bdffda61e6e5b
    28 schema:url http://link.springer.com/10.1007/3-540-44654-0_15
    29 sgo:license sg:explorer/license/
    30 sgo:sdDataset chapters
    31 rdf:type schema:Chapter
    32 N11d2c7d82b364db1891bdffda61e6e5b schema:name Springer Nature - SN SciGraph project
    33 rdf:type schema:Organization
    34 N1350b954c9774c3d959ae7acf4a7d44d rdf:first sg:person.013750414271.15
    35 rdf:rest rdf:nil
    36 N1621dabed5994928ba598ac0937e866c rdf:first N813a7a1772d74facadfa597f2fb296f3
    37 rdf:rest Nf7832838b6e34b0a8b193245c45be002
    38 N30aa3ca2d2964809b8863fe7eb409ba7 schema:name dimensions_id
    39 schema:value pub.1043896941
    40 rdf:type schema:PropertyValue
    41 N3550ed37d8eb4dcdaddf38c18b7fb55f schema:familyName Kakas
    42 schema:givenName Antonis C.
    43 rdf:type schema:Person
    44 N3e36d1e52e4b44e68e31e91de521a3f3 schema:familyName Monfroy
    45 schema:givenName Eric
    46 rdf:type schema:Person
    47 N44f366b799094fbf894c1c7b308d6657 rdf:first N9afd171e0567424e915e15376d594312
    48 rdf:rest rdf:nil
    49 N7cc8eb4b10ca4f53988b94088396f200 schema:name readcube_id
    50 schema:value d119287e2b87c75d5042dc7715c6d8c266bc6057dd18798e6e9ec71bb37ef27d
    51 rdf:type schema:PropertyValue
    52 N7e424659c3bd4548819672f685e2bf3a rdf:first N3550ed37d8eb4dcdaddf38c18b7fb55f
    53 rdf:rest N44f366b799094fbf894c1c7b308d6657
    54 N813a7a1772d74facadfa597f2fb296f3 schema:familyName Apt
    55 schema:givenName Krzysztof R.
    56 rdf:type schema:Person
    57 N9afd171e0567424e915e15376d594312 schema:familyName Rossi
    58 schema:givenName Francesca
    59 rdf:type schema:Person
    60 Nb14cd876d79c4774835f1dadc57562f7 schema:location Berlin, Heidelberg
    61 schema:name Springer Berlin Heidelberg
    62 rdf:type schema:Organisation
    63 Nb7e5c9060e48450697954c0420d98acb schema:name doi
    64 schema:value 10.1007/3-540-44654-0_15
    65 rdf:type schema:PropertyValue
    66 Nbef17545347f40abb464b2d68567b421 schema:isbn 978-3-540-44654-5
    67 978-3-540-67885-4
    68 schema:name New Trends in Constraints
    69 rdf:type schema:Book
    70 Nf7832838b6e34b0a8b193245c45be002 rdf:first N3e36d1e52e4b44e68e31e91de521a3f3
    71 rdf:rest N7e424659c3bd4548819672f685e2bf3a
    72 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    73 schema:name Information and Computing Sciences
    74 rdf:type schema:DefinedTerm
    75 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
    76 schema:name Computer Software
    77 rdf:type schema:DefinedTerm
    78 sg:person.013750414271.15 schema:affiliation https://www.grid.ac/institutes/grid.5252.0
    79 schema:familyName Frühwirth
    80 schema:givenName Thom
    81 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013750414271.15
    82 rdf:type schema:Person
    83 sg:pub.10.1007/bfb0017444 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010989701
    84 https://doi.org/10.1007/bfb0017444
    85 rdf:type schema:CreativeWork
    86 https://doi.org/10.1016/0004-3702(85)90041-4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004121645
    87 rdf:type schema:CreativeWork
    88 https://doi.org/10.1016/0743-1066(93)90014-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007843535
    89 rdf:type schema:CreativeWork
    90 https://doi.org/10.1016/0743-1066(94)90033-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004885944
    91 rdf:type schema:CreativeWork
    92 https://doi.org/10.1016/s0747-7171(87)80022-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1026818855
    93 rdf:type schema:CreativeWork
    94 https://www.grid.ac/institutes/grid.5252.0 schema:alternateName Ludwig Maximilian University of Munich
    95 schema:name Ludwig-Maximilians-Universität München, Oettingenstrasse 67, D-80538 Munich, Germany
    96 rdf:type schema:Organization
     




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


    ...