Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-24986
Titel: Unification theory
Verfasser: Baader, Franz
Sprache: Englisch
Erscheinungsjahr: 1992
Quelle: Kaiserslautern ; Saarbrücken : DFKI, 1992
SWD-Schlagwörter: Künstliche Intelligenz
DDC-Sachgruppe: 004 Informatik
Dokumentart : Report (Bericht)
Kurzfassung: The purpose of this paper is not to give an overview of the state of art in unification theory. It is intended to be a short introduction into the area of equational unification which should give the reader a feeling for what unification theory might be about. The basic notions such as complete and minimal complete sets of unifiers, and unification types of equational theories are introduced and illustrated by examples. Then we shall describe the original motivations for considering unification (in the empty theory) in resolution theorem proving and term rewriting. Starting with Robinson's first unification algorithm it will be sketched how more efficient unification algorithms can be derived. We shall then explain the reasons which lead to the introduction of unification in non-empty theories into the above mentioned areas theorem proving and term rewriting. For theory unification it makes a difference whether single equations or systems of equations are considered. In addition, one has to be careful with regard to the signature over which the terms of the unification problems can be built. This leads to the distinction between elementary unification, unification with constants, and general unification (where arbitrary free function symbols may occur). Going from elementary unification to general unification is an instance of the so-called combination problem for equational theories which can be formulated as follows: Let E, F be equational theories over disjoint signatures. How can unification algorithms for E, F be combined to a unification algorithm for the theory E cup F.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-37849
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Band: 92-33
SciDok-Publikation: 1-Jul-2011
Fakultät: SE - Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Fakultät / Institution:SciDok - Elektronische Dokumente der UdS

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
RR_92_33.pdf11,88 MBAdobe PDFÖffnen/Anzeigen

Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.