Please use this identifier to cite or link to this item: doi:10.22028/D291-24989
Title: Combination techniques and decision problems for disunification
Author(s): Baader, Franz
Schulz, Klaus U.
Language: English
Year of Publication: 1993
OPUS Source: Kaiserslautern ; Saarbrücken : DFKI, 1993
SWD key words: Künstliche Intelligenz
DDC notations: 004 Computer science, internet
Publikation type: Report
Abstract: 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 to this record: urn:nbn:de:bsz:291-scidok-37878
Series name: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Series volume: 93-05
Date of registration: 1-Jul-2011
Faculty: SE - Sonstige Einrichtungen
Department: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
RR_93_05.pdf15,4 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.