- Titel
- Unification Theory - An Introduction
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-792209
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 97-103
- Erstveröffentlichung
- 1997
- DOI
- https://doi.org/10.25368/2022.135
- Abstract (EN)
- Aus der Einleitung: „Equational unification is a generalization of syntactic unification in which semantic properties of function symbols are taken into account. For example, assume that the function symbol '+' is known to be commutative. Given the unication problem x + y ≐ a + b (where x and y are variables, and a and b are constants), an algorithm for syntactic unification would return the substitution {x ↦ a; y ↦ b} as the only (and most general) unifier: to make x + y and a + b syntactically equal, one must replace the variable x by a and y by b. However, commutativity of '+' implies that {x ↦ b; y ↦ b} also is a unifier in the sense that the terms obtained by its application, namely b + a and a + b, are equal modulo commutativity of '+'. More generally, equational unification is concerned with the problem of how to make terms equal modulo a given equational theory, which specifies semantic properties of the function symbols that occur in the terms to be unified.”
- Freie Schlagwörter (DE)
- Subsumtion, ALN-Konzept, Beschreibungslogik, strukturelle Charakterisierung
- Freie Schlagwörter (EN)
- subsumption, ALN-concept, description logic, structural characterization
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 136
- Publizierende Institution
- Aachen University of Technology, Aachen
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-792209
- Veröffentlichungsdatum Qucosa
- 19.05.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0