{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:23Z","timestamp":1747173443029,"version":"3.40.5"},"reference-count":32,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2022,3,24]],"date-time":"2022-03-24T00:00:00Z","timestamp":1648080000000},"content-version":"unspecified","delay-in-days":204,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,9]]},"abstract":"Abstract<\/jats:title>Ordering is a well-established concept in mathematics and also plays an important role in many areas of computer science, wherequasi-orderings<\/jats:italic>, most notablywell-founded quasi-orderings<\/jats:italic>andwell-quasi-orderings,<\/jats:italic>are of particular interest. This paper deals with quasi-orderings on first-order terms and introduces a new notion of unification based on a special quasi-order, known ashomeomorphic tree embedding<\/jats:italic>. Historically, the development of unification theory began with the central notion ofa most general unifier<\/jats:italic>based on thesubsumption order<\/jats:italic>. A unifier$\\sigma$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>is most general, if it subsumes any other unifier$\\tau$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, that is, if there is a substitution$\\lambda$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>with$\\tau=_{E}\\sigma\\lambda$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, where E is an equational theory and$=_{E}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>denotes equality under E. Since there is in general more than one most general unifier for unification problems under equational theories E, calledE-Unification<\/jats:italic>, we have the notion of a complete and minimal set of unifiers under E for a unification problem$\\varGamma$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, denoted as$\\mu\\mathcal{U}\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. This set is still the basic notion in unification theory today. But, unfortunately, the subsumption quasi-order is not a well-founded quasi-order, which is the reason why for certain equational theories there are solvable E-unification problems, but the set$\\mu\\mathcal{U}\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>does not exist. They are called type nullary in the unification hierarchy. In order to overcome this problem and also to substantially reduce the number of most general unifiers, we extended the well-knownencompassment order on terms<\/jats:italic>to anencompassment order on substitutions<\/jats:italic>(modulo E). Unification under the encompassment order is calledessential unification<\/jats:italic>and if$\\mu\\mathcal{U}\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>exists, then the complete set of essential unifiers$e\\mathcal{U}\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>is a subset of$\\mu\\mathcal{U}\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. An interesting effect is that many E-unification problems with an infinite set of most general unifiers (under the subsumption order) reduce to a problem with only finitely manyessential<\/jats:italic>unifiers. Moreover, there are cases of an equational theory E, for which the complete set of most general unifiers does not exist, theminimal and complete set of essential unifiers<\/jats:italic>however does exist. Unfortunately again, the encompassment order is not a well-founded quasi-ordering either, that is, there are still theories with a solvable unification problem, for which a minimal and complete set of essential unifiers does not exist. This paper deals with a third approach, namely the extension of the well-knownhomeomorphic embedding of terms<\/jats:italic>to ahomeomorphic embedding of substitutions (modulo E)<\/jats:italic>. We examine the set of most general, minimal, and complete E-unifiers under the quasi-order of homeomorphic embedment modulo an equational theory E, called$\\varphi U\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, and propose an appropriate definitional framework based on the standard notions of unification theory extended by notions for thetree embedding theorem<\/jats:italic>or Kruskal\u2019s theorem as it is called. The main results are that forregular<\/jats:italic>theories the minimal and complete set$\\varphi\\mathcal{U}\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>always exists. If we restrict the E-embedding order topure E-embedding, a<\/jats:italic>well-known technique in logic programming and term rewriting where the difference between variables is ignored, the set$\\varphi_{\\pi}\\mathcal{U}\\Sigma_{E}(\\Gamma)$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>always exists and it is even finite for any theory E.<\/jats:p>","DOI":"10.1017\/s0960129522000019","type":"journal-article","created":{"date-parts":[[2022,3,25]],"date-time":"2022-03-25T03:52:06Z","timestamp":1648180326000},"page":"898-917","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["E-Unification based on Generalized Embedding"],"prefix":"10.1017","volume":"31","author":[{"given":"Peter","family":"Szabo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6398-3284","authenticated-orcid":false,"given":"J\u00f6rg","family":"Siekmann","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2022,3,24]]},"reference":[{"key":"S0960129522000019_ref25","doi-asserted-by":"crossref","unstructured":"Leuschel, M. (1998). Improving homeomorphic embedding for online termination. In: International Workshop on Logic Programming Synthesis and Transformation. Berlin, Heidelberg: Springer.","DOI":"10.1007\/3-540-48958-4_11"},{"key":"S0960129522000019_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"S0960129522000019_ref30","first-page":"93","article-title":"Simplified proof of Kruskals tree theorem","volume":"3","author":"Singh","year":"2013","journal-title":"Mathematical Theory and Modeling"},{"key":"S0960129522000019_ref2","unstructured":"Alpuente, M. , Cuenca-Ortega, A. , Escobar, S. and Meseguer, J. (2018). Homeomorphic embedding modulo combinations of associativity and commutativity axioms. In: International Symposium on Logic-Based Program Synthesis and Transformation. Springer, pp. 38\u201355."},{"key":"S0960129522000019_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90022-E"},{"key":"S0960129522000019_ref23","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem and V\u00c1zsonyi\u2019s conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0960129522000019_ref4","article-title":"Unification in modal and description logics","volume":"19","author":"Baader","year":"2011","journal-title":"Logic Journal of GPL"},{"key":"S0960129522000019_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S0960129522000019_ref31","unstructured":"Szabo, P. , Siekmann, J. and Hoche, M. (2016). What is essential unification? In: Martin Davis on Computability, Computation, and Computational Logic. Springer\u2019s Series \u201cOutstanding Contributions to Logic\u201d."},{"key":"S0960129522000019_ref18","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"first-page":"82","year":"2008","author":"Hoche","key":"S0960129522000019_ref19"},{"key":"S0960129522000019_ref9","article-title":"Exact unification and admissibility","volume":"11","author":"Cabrer","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129522000019_ref20","unstructured":"Hoche, M. , Siekmann, J. and Szabo, P. (2016). String unification is essentially infinitary. IFCoLog Journal of Logics and their Applications."},{"key":"S0960129522000019_ref8","unstructured":"Cabrer, L. M. and Metcalfe, G. (2014). From admissibility to a new hierarchy of unification types. RISC 41,Linz."},{"key":"S0960129522000019_ref13","first-page":"162","article-title":"Notations for rewriting","volume":"43","author":"Dershowitz","year":"1991","journal-title":"Bulletin of the EATCS"},{"year":"2002","author":"Leuschel","key":"S0960129522000019_ref26"},{"key":"S0960129522000019_ref16","unstructured":"Ghilardi, S. (2018). Handling substitutions via duality. In: Proceedings of the International Workshop on Unification Theory (UNIF32), FLoC2018, Oxford."},{"year":"2016","author":"Alpuente","key":"S0960129522000019_ref1"},{"key":"S0960129522000019_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"S0960129522000019_ref14","unstructured":"Gallier, J. H. (1991). Unification procedures in automated deduction methods based on matings: A survey. Technical Report CIS-436, University of Pennsylvania, Department of Computer and Information Science."},{"key":"S0960129522000019_ref6","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/oso\/9780198537465.003.0002","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"Baader","year":"1994"},{"year":"2001","author":"Baader","key":"S0960129522000019_ref7"},{"key":"S0960129522000019_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90098-1"},{"journal-title":"Mathematical Structures in Computer Science.","article-title":"E-Unification based on Generalized Embedding","author":"Szabo","key":"S0960129522000019_ref32"},{"key":"S0960129522000019_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"first-page":"833","year":"1963","author":"Nash-Williams","key":"S0960129522000019_ref27"},{"key":"S0960129522000019_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2004.12.001"},{"key":"S0960129522000019_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80012-4"},{"key":"S0960129522000019_ref17","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.6.733"},{"key":"S0960129522000019_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(72)90063-5"},{"key":"S0960129522000019_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/62029.62030"},{"key":"S0960129522000019_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000019","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,19]],"date-time":"2023-11-19T06:49:03Z","timestamp":1700376543000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000019\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9]]},"references-count":32,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["S0960129522000019"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000019","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2021,9]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}