Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-39846
Titel: | The Undecidability of the [D A]-Unification Problem |
VerfasserIn: | Siekmann, Jörg Szabo, P. |
Sprache: | Englisch |
Erscheinungsjahr: | 1986 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | We show that the DA-Unification problem is undecidable. That is, given two binary function symbols Φ and Θ, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following DA-axioms hold: (x Φ y) Θ z = (x Θ z) Φ (y Θ z) x Θ (y Φ z) = (x Θ y) Φ (x Θ z) x Φ (y Φ z) = (x Φ y) Φ z Two terms are DA-unifiable (i.e. an equation is solvable in DA) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory DA. This is the smallest currently known axiomatic subset of Hilbert's Tenth Problem for which an undecidability result has been obtained. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-398463 hdl:20.500.11880/37662 http://dx.doi.org/10.22028/D291-39846 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 86,19 |
Datum des Eintrags: | 17-Mai-2024 |
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-86-19_Siekmann-Szabo_The-Undecidability-of-the-[D A]-Unification-Problem.pdf | 7,14 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.