Ontology type: schema:ScholarlyArticle
2021-09-25
AUTHORSMaría Alpuente, Santiago Escobar, José Meseguer, Julia Sapiña
ABSTRACTGeneralization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t′\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$t^{\prime }$\end{document} is a term t′′\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$t^{\prime \prime }$\end{document} of which t and t′\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$t^{\prime }$\end{document} are substitution instances. The dual of most general equational unifiers is that of least general equational generalizers, i.e., most specific anti-instances modulo equations. In a previous work, we extended the classical untyped generalization algorithm to: (1) an order-sorted typed setting with sorts, subsorts, and subtype polymorphism; (2) work modulo equational theories, where function symbols can obey any combination of associativity, commutativity, and identity axioms (including the empty set of such axioms); and (3) the combination of both, which results in a modular, order-sorted equational generalization algorithm. However, Cerna and Kutsia showed that our algorithm is generally incomplete for the case of identity axioms and a counterexample was given. Furthermore, they proved that, in theories with two identity elements or more, generalization with identity axioms is generally nullary, yet it is finitary for both the linear and one-unital fragments, i.e., either solutions with repeated variables are disregarded or the considered theories are restricted to having just one function symbol with an identity or unit element. In this work, we show how we can easily extend our original inference system to cope with the non-linear fragment and identify a more general class than one–unit theories where generalization with identity axioms is finitary. More... »
PAGES499-522
http://scigraph.springernature.com/pub.10.1007/s10472-021-09771-1
DOIhttp://dx.doi.org/10.1007/s10472-021-09771-1
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1141395264
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/01",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Mathematical Sciences",
"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"
},
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0102",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Applied Mathematics",
"type": "DefinedTerm"
},
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Artificial Intelligence and Image Processing",
"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": "Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Spain",
"id": "http://www.grid.ac/institutes/grid.157927.f",
"name": [
"Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Spain"
],
"type": "Organization"
},
"familyName": "Alpuente",
"givenName": "Mar\u00eda",
"id": "sg:person.010344015011.31",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010344015011.31"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Spain",
"id": "http://www.grid.ac/institutes/grid.157927.f",
"name": [
"Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Spain"
],
"type": "Organization"
},
"familyName": "Escobar",
"givenName": "Santiago",
"id": "sg:person.016354322055.39",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016354322055.39"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "University of Illinois at Urbana-Champaign, Champaign, IL, USA",
"id": "http://www.grid.ac/institutes/grid.35403.31",
"name": [
"University of Illinois at Urbana-Champaign, Champaign, IL, USA"
],
"type": "Organization"
},
"familyName": "Meseguer",
"givenName": "Jos\u00e9",
"id": "sg:person.013667315414.11",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013667315414.11"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Spain",
"id": "http://www.grid.ac/institutes/grid.157927.f",
"name": [
"Universitat Polit\u00e8cnica de Val\u00e8ncia, Val\u00e8ncia, Spain"
],
"type": "Organization"
},
"familyName": "Sapi\u00f1a",
"givenName": "Julia",
"id": "sg:person.015213402353.49",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015213402353.49"
],
"type": "Person"
}
],
"citation": [
{
"id": "sg:pub.10.1007/978-3-319-11558-0_40",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1018933075",
"https://doi.org/10.1007/978-3-319-11558-0_40"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-04222-5_15",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1043246740",
"https://doi.org/10.1007/978-3-642-04222-5_15"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-030-19570-0_11",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1113961918",
"https://doi.org/10.1007/978-3-030-19570-0_11"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-642-00515-2_3",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1032808765",
"https://doi.org/10.1007/978-3-642-00515-2_3"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-74141-1_3",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1001845241",
"https://doi.org/10.1007/978-3-540-74141-1_3"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s11786-020-00455-3",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1124668992",
"https://doi.org/10.1007/s11786-020-00455-3"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-64299-4_26",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1002824877",
"https://doi.org/10.1007/3-540-64299-4_26"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/s10994-011-5274-3",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1031185551",
"https://doi.org/10.1007/s10994-011-5274-3"
],
"type": "CreativeWork"
}
],
"datePublished": "2021-09-25",
"datePublishedReg": "2021-09-25",
"description": "Generalization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t\u2032\\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$t^{\\prime }$\\end{document} is a term t\u2032\u2032\\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$t^{\\prime \\prime }$\\end{document} of which t and t\u2032\\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$t^{\\prime }$\\end{document} are substitution instances. The dual of most general equational unifiers is that of least general equational generalizers, i.e., most specific anti-instances modulo equations. In a previous work, we extended the classical untyped generalization algorithm to: (1) an order-sorted typed setting with sorts, subsorts, and subtype polymorphism; (2) work modulo equational theories, where function symbols can obey any combination of associativity, commutativity, and identity axioms (including the empty set of such axioms); and (3) the combination of both, which results in a modular, order-sorted equational generalization algorithm. However, Cerna and Kutsia showed that our algorithm is generally incomplete for the case of identity axioms and a counterexample was given. Furthermore, they proved that, in theories with two identity elements or more, generalization with identity axioms is generally nullary, yet it is finitary for both the linear and one-unital fragments, i.e., either solutions with repeated variables are disregarded or the considered theories are restricted to having just one function symbol with an identity or unit element. In this work, we show how we can easily extend our original inference system to cope with the non-linear fragment and identify a more general class than one\u2013unit theories where generalization with identity axioms is finitary.",
"genre": "article",
"id": "sg:pub.10.1007/s10472-021-09771-1",
"inLanguage": "en",
"isAccessibleForFree": false,
"isPartOf": [
{
"id": "sg:journal.1043955",
"issn": [
"1012-2443",
"1573-7470"
],
"name": "Annals of Mathematics and Artificial Intelligence",
"publisher": "Springer Nature",
"type": "Periodical"
},
{
"issueNumber": "5",
"type": "PublicationIssue"
},
{
"type": "PublicationVolume",
"volumeNumber": "90"
}
],
"keywords": [
"symbols",
"identity element",
"identity",
"unifiers",
"work",
"sort",
"theory",
"function symbols",
"unification",
"generalizers",
"term t",
"instances",
"subsorts",
"axioms",
"elements",
"generalization",
"terms",
"equational theory",
"class",
"previous work",
"generalization algorithm",
"subtype polymorphism",
"polymorphism",
"combination",
"associativity",
"ceRNA",
"cases",
"counterexamples",
"fragments",
"variables",
"system",
"algorithm",
"commutativity",
"solution",
"dual",
"modulo equations",
"equations",
"identity axioms",
"unit element",
"inference system",
"general class",
"substitution instances",
"modulo equational theories",
"combination of associativity"
],
"name": "Order-sorted equational generalization algorithm revisited",
"pagination": "499-522",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1141395264"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/s10472-021-09771-1"
]
}
],
"sameAs": [
"https://doi.org/10.1007/s10472-021-09771-1",
"https://app.dimensions.ai/details/publication/pub.1141395264"
],
"sdDataset": "articles",
"sdDatePublished": "2022-05-20T07:38",
"sdLicense": "https://scigraph.springernature.com/explorer/license/",
"sdPublisher": {
"name": "Springer Nature - SN SciGraph project",
"type": "Organization"
},
"sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/article/article_906.jsonl",
"type": "ScholarlyArticle",
"url": "https://doi.org/10.1007/s10472-021-09771-1"
}
]Download the RDF metadata as: json-ld nt turtle xml License info
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-09771-1'
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-09771-1'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10472-021-09771-1'
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-09771-1'
This table displays all metadata directly associated to this object as RDF triples.
170 TRIPLES
22 PREDICATES
80 URIs
61 LITERALS
6 BLANK NODES