Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-24989
Titel: Combination techniques and decision problems for disunification
Verfasser: Baader, Franz
Schulz, Klaus U.
Sprache: Englisch
Erscheinungsjahr: 1993
Quelle: Kaiserslautern ; Saarbrücken : DFKI, 1993
SWD-Schlagwörter: Künstliche Intelligenz
DDC-Sachgruppe: 004 Informatik
Dokumentart : Report (Bericht)
Kurzfassung: Previous work on combination techniques considered the question of how to combine unification algorithms for disjoint equational theories E_{1} ,...,E_{n} in order to obtain a unification algorithm for the union E1 unified ... unified En of the theories. Here we want to show that variants of this method may be used to decide solvability and ground solvability of disunification problems in E_{1}cup...cup E_{n}. Our first result says that solvability of disunification problems in the free algebra of the combined theory E_{1}cup...cup E_{n} is decidable if solvability of disunification problems with linear constant restrictions in the free algebras of the theories E_{i}(i = 1,...,n) is decidable. In order to decide ground solvability (i.e., solvability in the initial algebra) of disunification problems in E_{1}cup...cup E_{n} we have to consider a new kind of subproblem for the particular theories Ei, namely solvability (in the free algebra) of disunification problems with linear constant restriction under the additional constraint that values of variables are not Ei-equivalent to variables. The correspondence between ground solvability and this new kind of solvability holds, (1) if one theory Ei is the free theory with at least one function symbol and one constant, or (2) if the initial algebras of all theories Ei are infinite. Our results can be used to show that the existential fragment of the theory of the (ground) term algebra modulo associativity of a finite number of function symbols is decidable; the same result follows for function symbols which are associative and commutative, or associative, commutative and idempotent.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-37878
hdl:20.500.11880/25045
http://dx.doi.org/10.22028/D291-24989
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Band: 93-05
SciDok-Publikation: 1-Jul-2011
Fakultät: Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Fakultät / Institution:SE - Sonstige Einrichtungen

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
RR_93_05.pdf15,4 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.