Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40194
Titel: | Unification of Term Schemes - Theory and Applications |
VerfasserIn: | Gramlich, Bernhard |
Sprache: | Englisch |
Erscheinungsjahr: | 1988 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | We present a new approach for solving certain infinite sets of first order unification problems represented by term schemes. Within the framework of second order equational logic solving such scheme unification problems amounts exactly to solving (variable-) restricted unification problems. A method known for solving first order restricted unification problems is generalized to the second order case. Essentially this is achieved by transforming a restricted unification problem into an unrestricted one, solving the latter and retransforming the solutions obtained. The results on second order restricted unification are then used to solve the original problem, namely to decide the solvability of scheme unification problems and - in the positive case - to compute the corresponding most general unifiers. Finally the results are applied to provide sufficient conditions for a property of "repeated unifiability” which in turn is crucial for the analysis of divergence of completion procedures for term rewriting systems. Although the study of divergent completion behaviour was the starting point for the work presented, the results obtained are not only applicable to divergence analysis but may be useful for other applications, too. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-401944 hdl:20.500.11880/36239 http://dx.doi.org/10.22028/D291-40194 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 88,18 |
Datum des Eintrags: | 11-Aug-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-88-18_Gramlich_Unification-of-Term-Schemes-Theory-and-Applications.pdf | 1,59 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.