Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40373
Titel: | Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems |
VerfasserIn: | Baader, Franz |
Sprache: | Englisch |
Erscheinungsjahr: | 1990 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | We define E-unification, weak E-unification, E-upper bound, E-lower bound and E-generalization problems and the corresponding notions of unification, weak unification, upper bound, lower bound and generalization type of an equational theory. Most general unifiers, most general weak unifiers, suprema, infima and most specific generalizers correspond to "weak versions" of well-known categorical concepts. The problems are first studied for the empty theory using the restricted instantiation ordering ( i.e., substitutions are compared w.r.t. their behaviour on finite sets of variables ) and the unrestricted instantiation ordering ( i.e., substitutions are compared w.r.t. their behaviour on all variables ). This shows that the unrestricted instantiation ordering should only be used for unification. For the other problems the restricted ordering yields much better results. We shall also show that there exists an equational theory where unification problems always have most general unifiers w.r.t. the restricted instantiation ordering but not w.r.t. the unrestricted instantiation ordering. This accounts for the fact that equational unification is mostly done with restricted instantiation. Most general unifiers ( i.e., weak coequalizers ) modulo commutative theories cannot always be chosen as coequalizers. But we can give algebraic conditions under which this is possible. For the class of commutative theories there always exist least specific generalizers. That means that all commutative theories have generalization type "unitary". |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-403731 hdl:20.500.11880/36389 http://dx.doi.org/10.22028/D291-40373 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 90,2 |
Datum des Eintrags: | 5-Sep-2023 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI-Report-SR-90-02_Baader_Unification-Weak-Unification-Upper-Bound-Lower-Bound-and-Generalization-Problems.pdf | 5,56 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.