Functions-as-constructors higher-order unification: extended pattern unification View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2021-09-30

AUTHORS

Tomer Libal, Dale Miller

ABSTRACT

Unification is a central operation in constructing a range of computational logic systems based on first-order and higher-order logics. First-order unification has several properties that guide its incorporation in such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respects the laws governing λ-binding (i.e., the equalities for α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been used in numerous implemented systems and in various theoretical settings, it is too weak for many applications. This paper defines an extension of pattern unification that should make it more generally applicable, especially in proof assistants that allow for higher-order functions. This extension’s main idea is that the arguments to a higher-order, free variable can be more than just distinct bound variables. In particular, such arguments can be terms constructed from (sufficient numbers of) such bound variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above. More... »

PAGES

1-25

References to SciGraph publications

  • 2007-01-01. Crafting a Proof Assistant in TYPES FOR PROOFS AND PROGRAMS
  • 2011. Higher-Order Dynamic Pattern Unification for Dependent Types and Records in TYPED LAMBDA CALCULI AND APPLICATIONS
  • 2012. Satallax: An Automatic Higher-Order Prover in AUTOMATED REASONING
  • 1991-08. Ellipsis and higher-order unification in LINGUISTICS AND PHILOSOPHY
  • 2009. Hints in Unification in THEOREM PROVING IN HIGHER ORDER LOGICS
  • 1993. Linear unification of higher-order patterns in TAPSOFT'93: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT
  • 2009. A Brief Overview of Agda – A Functional Language with Dependent Types in THEOREM PROVING IN HIGHER ORDER LOGICS
  • 2010-07-13. Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) in AUTOMATED REASONING
  • 2008. Canonical Big Operators in THEOREM PROVING IN HIGHER ORDER LOGICS
  • 1999. System Description: Teyjus—A Compiler and Abstract Machine Based Implementation of λProlog in AUTOMATED DEDUCTION — CADE-16
  • 2016-09-05. Proof checking and logic programming in FORMAL ASPECTS OF COMPUTING
  • 1998. System description: Leo — A higher-order theorem prover in AUTOMATED DEDUCTION — CADE-15
  • 1986. The TPS theorem proving system in 8TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
  • 1999. System Description: Twelf — A Meta-Logical Framework for Deductive Systems in AUTOMATED DEDUCTION — CADE-16
  • 1978-03. Proving and applying program transformations expressed with second-order patterns in ACTA INFORMATICA
  • 1996. Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type in REWRITING TECHNIQUES AND APPLICATIONS
  • 2006. Minlog in THE SEVENTEEN PROVERS OF THE WORLD
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s10472-021-09774-y

    DOI

    http://dx.doi.org/10.1007/s10472-021-09774-y

    DIMENSIONS

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


    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": "University of Luxembourg, Belval, Luxembourg", 
              "id": "http://www.grid.ac/institutes/grid.16008.3f", 
              "name": [
                "University of Luxembourg, Belval, Luxembourg"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Libal", 
            "givenName": "Tomer", 
            "id": "sg:person.010201654626.94", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010201654626.94"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Inria Saclay, LIX/\u00c9cole Polytechnique, Palaiseau, France", 
              "id": "http://www.grid.ac/institutes/grid.457355.5", 
              "name": [
                "Inria Saclay, LIX/\u00c9cole Polytechnique, Palaiseau, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Miller", 
            "givenName": "Dale", 
            "id": "sg:person.07476663267.12", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07476663267.12"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/s00165-016-0393-z", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1031379677", 
              "https://doi.org/10.1007/s00165-016-0393-z"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-48660-7_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012080372", 
              "https://doi.org/10.1007/3-540-48660-7_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11542384_19", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006435437", 
              "https://doi.org/10.1007/11542384_19"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-71067-7_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1032888125", 
              "https://doi.org/10.1007/978-3-540-71067-7_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0054256", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1046446726", 
              "https://doi.org/10.1007/bfb0054256"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-74464-1_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038014207", 
              "https://doi.org/10.1007/978-3-540-74464-1_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00264598", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1052329404", 
              "https://doi.org/10.1007/bf00264598"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-48660-7_25", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1025470247", 
              "https://doi.org/10.1007/3-540-48660-7_25"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-03359-9_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049860781", 
              "https://doi.org/10.1007/978-3-642-03359-9_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-21691-6_5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006060170", 
              "https://doi.org/10.1007/978-3-642-21691-6_5"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-16780-3_128", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010676765", 
              "https://doi.org/10.1007/3-540-16780-3_128"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-14203-1_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1046659196", 
              "https://doi.org/10.1007/978-3-642-14203-1_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-31365-3_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008150028", 
              "https://doi.org/10.1007/978-3-642-31365-3_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-56610-4_78", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022301333", 
              "https://doi.org/10.1007/3-540-56610-4_78"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-61464-8_64", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038860674", 
              "https://doi.org/10.1007/3-540-61464-8_64"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-03359-9_8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027412794", 
              "https://doi.org/10.1007/978-3-642-03359-9_8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00630923", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1014274890", 
              "https://doi.org/10.1007/bf00630923"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2021-09-30", 
        "datePublishedReg": "2021-09-30", 
        "description": "Unification is a central operation in constructing a range of computational logic systems based on first-order and higher-order logics. First-order unification has several properties that guide its incorporation in such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respects the laws governing \u03bb-binding (i.e., the equalities for \u03b1, \u03b2, and \u03b7-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been used in numerous implemented systems and in various theoretical settings, it is too weak for many applications. This paper defines an extension of pattern unification that should make it more generally applicable, especially in proof assistants that allow for higher-order functions. This extension\u2019s main idea is that the arguments to a higher-order, free variable can be more than just distinct bound variables. In particular, such arguments can be terms constructed from (sufficient numbers of) such bound variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s10472-021-09774-y", 
        "inLanguage": "en", 
        "isAccessibleForFree": true, 
        "isPartOf": [
          {
            "id": "sg:journal.1043955", 
            "issn": [
              "1012-2443", 
              "1573-7470"
            ], 
            "name": "Annals of Mathematics and Artificial Intelligence", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }
        ], 
        "keywords": [
          "logic system", 
          "term constructors", 
          "theoretical setting", 
          "free variables", 
          "main idea", 
          "such systems", 
          "first-order unification", 
          "term structure", 
          "central operation", 
          "unification", 
          "extension", 
          "bound variables", 
          "small extension", 
          "proof assistant", 
          "higher-order logic", 
          "satisfies", 
          "properties", 
          "variables", 
          "higher-order unification", 
          "unifiers", 
          "system", 
          "pattern fragments", 
          "function", 
          "higher-order functions", 
          "law", 
          "argument", 
          "pattern subsets", 
          "terms", 
          "applications", 
          "idea", 
          "structure", 
          "operation", 
          "subset", 
          "subterms", 
          "search", 
          "range", 
          "logic", 
          "constructors", 
          "such arguments", 
          "setting", 
          "incorporation", 
          "fragments", 
          "assistants", 
          "binding", 
          "typing", 
          "paper", 
          "computational logic systems", 
          "untyped term structures", 
          "full higher-order unification", 
          "term-level typing", 
          "pattern unification", 
          "such bound variables", 
          "unification satisfies", 
          "constructors higher-order unification", 
          "extended pattern unification"
        ], 
        "name": "Functions-as-constructors higher-order unification: extended pattern unification", 
        "pagination": "1-25", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1141519417"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s10472-021-09774-y"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s10472-021-09774-y", 
          "https://app.dimensions.ai/details/publication/pub.1141519417"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-01-01T19:03", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/article/article_902.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s10472-021-09774-y"
      }
    ]
     

    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/s10472-021-09774-y'

    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/s10472-021-09774-y'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10472-021-09774-y'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10472-021-09774-y'


     

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

    185 TRIPLES      22 PREDICATES      95 URIs      70 LITERALS      4 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s10472-021-09774-y schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Nddf936031f174e40951ff65470420440
    4 schema:citation sg:pub.10.1007/11542384_19
    5 sg:pub.10.1007/3-540-16780-3_128
    6 sg:pub.10.1007/3-540-48660-7_14
    7 sg:pub.10.1007/3-540-48660-7_25
    8 sg:pub.10.1007/3-540-56610-4_78
    9 sg:pub.10.1007/3-540-61464-8_64
    10 sg:pub.10.1007/978-3-540-71067-7_11
    11 sg:pub.10.1007/978-3-540-74464-1_2
    12 sg:pub.10.1007/978-3-642-03359-9_6
    13 sg:pub.10.1007/978-3-642-03359-9_8
    14 sg:pub.10.1007/978-3-642-14203-1_2
    15 sg:pub.10.1007/978-3-642-21691-6_5
    16 sg:pub.10.1007/978-3-642-31365-3_11
    17 sg:pub.10.1007/bf00264598
    18 sg:pub.10.1007/bf00630923
    19 sg:pub.10.1007/bfb0054256
    20 sg:pub.10.1007/s00165-016-0393-z
    21 schema:datePublished 2021-09-30
    22 schema:datePublishedReg 2021-09-30
    23 schema:description Unification is a central operation in constructing a range of computational logic systems based on first-order and higher-order logics. First-order unification has several properties that guide its incorporation in such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respects the laws governing λ-binding (i.e., the equalities for α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been used in numerous implemented systems and in various theoretical settings, it is too weak for many applications. This paper defines an extension of pattern unification that should make it more generally applicable, especially in proof assistants that allow for higher-order functions. This extension’s main idea is that the arguments to a higher-order, free variable can be more than just distinct bound variables. In particular, such arguments can be terms constructed from (sufficient numbers of) such bound variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.
    24 schema:genre article
    25 schema:inLanguage en
    26 schema:isAccessibleForFree true
    27 schema:isPartOf sg:journal.1043955
    28 schema:keywords applications
    29 argument
    30 assistants
    31 binding
    32 bound variables
    33 central operation
    34 computational logic systems
    35 constructors
    36 constructors higher-order unification
    37 extended pattern unification
    38 extension
    39 first-order unification
    40 fragments
    41 free variables
    42 full higher-order unification
    43 function
    44 higher-order functions
    45 higher-order logic
    46 higher-order unification
    47 idea
    48 incorporation
    49 law
    50 logic
    51 logic system
    52 main idea
    53 operation
    54 paper
    55 pattern fragments
    56 pattern subsets
    57 pattern unification
    58 proof assistant
    59 properties
    60 range
    61 satisfies
    62 search
    63 setting
    64 small extension
    65 structure
    66 subset
    67 subterms
    68 such arguments
    69 such bound variables
    70 such systems
    71 system
    72 term constructors
    73 term structure
    74 term-level typing
    75 terms
    76 theoretical setting
    77 typing
    78 unification
    79 unification satisfies
    80 unifiers
    81 untyped term structures
    82 variables
    83 schema:name Functions-as-constructors higher-order unification: extended pattern unification
    84 schema:pagination 1-25
    85 schema:productId N18520b12ed004e9fb7e42736190e43c2
    86 N88938a1547454828932917b4d42806cb
    87 schema:sameAs https://app.dimensions.ai/details/publication/pub.1141519417
    88 https://doi.org/10.1007/s10472-021-09774-y
    89 schema:sdDatePublished 2022-01-01T19:03
    90 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    91 schema:sdPublisher N7026a3a58ef242119d5e56d8b7a86454
    92 schema:url https://doi.org/10.1007/s10472-021-09774-y
    93 sgo:license sg:explorer/license/
    94 sgo:sdDataset articles
    95 rdf:type schema:ScholarlyArticle
    96 N18520b12ed004e9fb7e42736190e43c2 schema:name dimensions_id
    97 schema:value pub.1141519417
    98 rdf:type schema:PropertyValue
    99 N7026a3a58ef242119d5e56d8b7a86454 schema:name Springer Nature - SN SciGraph project
    100 rdf:type schema:Organization
    101 N88938a1547454828932917b4d42806cb schema:name doi
    102 schema:value 10.1007/s10472-021-09774-y
    103 rdf:type schema:PropertyValue
    104 Ncecc9b2512d2466b8d7dc974f736a5af rdf:first sg:person.07476663267.12
    105 rdf:rest rdf:nil
    106 Nddf936031f174e40951ff65470420440 rdf:first sg:person.010201654626.94
    107 rdf:rest Ncecc9b2512d2466b8d7dc974f736a5af
    108 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    109 schema:name Information and Computing Sciences
    110 rdf:type schema:DefinedTerm
    111 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    112 schema:name Computation Theory and Mathematics
    113 rdf:type schema:DefinedTerm
    114 sg:journal.1043955 schema:issn 1012-2443
    115 1573-7470
    116 schema:name Annals of Mathematics and Artificial Intelligence
    117 schema:publisher Springer Nature
    118 rdf:type schema:Periodical
    119 sg:person.010201654626.94 schema:affiliation grid-institutes:grid.16008.3f
    120 schema:familyName Libal
    121 schema:givenName Tomer
    122 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010201654626.94
    123 rdf:type schema:Person
    124 sg:person.07476663267.12 schema:affiliation grid-institutes:grid.457355.5
    125 schema:familyName Miller
    126 schema:givenName Dale
    127 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07476663267.12
    128 rdf:type schema:Person
    129 sg:pub.10.1007/11542384_19 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006435437
    130 https://doi.org/10.1007/11542384_19
    131 rdf:type schema:CreativeWork
    132 sg:pub.10.1007/3-540-16780-3_128 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010676765
    133 https://doi.org/10.1007/3-540-16780-3_128
    134 rdf:type schema:CreativeWork
    135 sg:pub.10.1007/3-540-48660-7_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012080372
    136 https://doi.org/10.1007/3-540-48660-7_14
    137 rdf:type schema:CreativeWork
    138 sg:pub.10.1007/3-540-48660-7_25 schema:sameAs https://app.dimensions.ai/details/publication/pub.1025470247
    139 https://doi.org/10.1007/3-540-48660-7_25
    140 rdf:type schema:CreativeWork
    141 sg:pub.10.1007/3-540-56610-4_78 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022301333
    142 https://doi.org/10.1007/3-540-56610-4_78
    143 rdf:type schema:CreativeWork
    144 sg:pub.10.1007/3-540-61464-8_64 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038860674
    145 https://doi.org/10.1007/3-540-61464-8_64
    146 rdf:type schema:CreativeWork
    147 sg:pub.10.1007/978-3-540-71067-7_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1032888125
    148 https://doi.org/10.1007/978-3-540-71067-7_11
    149 rdf:type schema:CreativeWork
    150 sg:pub.10.1007/978-3-540-74464-1_2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038014207
    151 https://doi.org/10.1007/978-3-540-74464-1_2
    152 rdf:type schema:CreativeWork
    153 sg:pub.10.1007/978-3-642-03359-9_6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049860781
    154 https://doi.org/10.1007/978-3-642-03359-9_6
    155 rdf:type schema:CreativeWork
    156 sg:pub.10.1007/978-3-642-03359-9_8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027412794
    157 https://doi.org/10.1007/978-3-642-03359-9_8
    158 rdf:type schema:CreativeWork
    159 sg:pub.10.1007/978-3-642-14203-1_2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1046659196
    160 https://doi.org/10.1007/978-3-642-14203-1_2
    161 rdf:type schema:CreativeWork
    162 sg:pub.10.1007/978-3-642-21691-6_5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006060170
    163 https://doi.org/10.1007/978-3-642-21691-6_5
    164 rdf:type schema:CreativeWork
    165 sg:pub.10.1007/978-3-642-31365-3_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008150028
    166 https://doi.org/10.1007/978-3-642-31365-3_11
    167 rdf:type schema:CreativeWork
    168 sg:pub.10.1007/bf00264598 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052329404
    169 https://doi.org/10.1007/bf00264598
    170 rdf:type schema:CreativeWork
    171 sg:pub.10.1007/bf00630923 schema:sameAs https://app.dimensions.ai/details/publication/pub.1014274890
    172 https://doi.org/10.1007/bf00630923
    173 rdf:type schema:CreativeWork
    174 sg:pub.10.1007/bfb0054256 schema:sameAs https://app.dimensions.ai/details/publication/pub.1046446726
    175 https://doi.org/10.1007/bfb0054256
    176 rdf:type schema:CreativeWork
    177 sg:pub.10.1007/s00165-016-0393-z schema:sameAs https://app.dimensions.ai/details/publication/pub.1031379677
    178 https://doi.org/10.1007/s00165-016-0393-z
    179 rdf:type schema:CreativeWork
    180 grid-institutes:grid.16008.3f schema:alternateName University of Luxembourg, Belval, Luxembourg
    181 schema:name University of Luxembourg, Belval, Luxembourg
    182 rdf:type schema:Organization
    183 grid-institutes:grid.457355.5 schema:alternateName Inria Saclay, LIX/École Polytechnique, Palaiseau, France
    184 schema:name Inria Saclay, LIX/École Polytechnique, Palaiseau, France
    185 rdf:type schema:Organization
     




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


    ...