Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-24828
Titel: Unification in the union of disjoint equational theories : combining decision procedures
Verfasser: Baader, Franz
Schulz, Klaus
Sprache: Englisch
Erscheinungsjahr: 1991
Quelle: Kaiserslautern ; Saarbrücken : DFKI, 1991
SWD-Schlagwörter: Künstliche Intelligenz
Approximationsalgorithmus
DDC-Sachgruppe: 004 Informatik
Dokumentart : Report (Bericht)
Kurzfassung: Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms which compute finite complete sets of unifiers. Thus the developed combination methods usually cannot be used to combine decision procedures, i.e., algorithms which just decide solvability of unification problems without computing unifiers. In this paper we describe a combination algorithm for decision procedures which works for arbitrary equational theories, provided that solvability of so-called unification problems with constant restrictions--a slight generalization of unification problems with constants--is decidable for these theories. As a consequence of this new method, we can for example show that general A-unifiability, i.e., solvability of A-unification problems with free function symbols, is decidable. Here A stands for the equational theory of one associative function symbol. Our method can also be used to combine algorithms which compute finite complete sets of unifiers. Manfred Schmidt-Schauß' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact. We also get the new result that unification in the union of disjoint equational theories is finitary, if general unification--i.e., unification of terms with additional free function symbols--is finitary in the single theories.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-35757
hdl:20.500.11880/24884
http://dx.doi.org/10.22028/D291-24828
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Band: 91-33
SciDok-Publikation: 16-Mai-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_91_33.pdf16,24 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.