Please use this identifier to cite or link to this item: doi:10.22028/D291-24986
Title: Unification theory
Author(s): Baader, Franz
Language: English
Year of Publication: 1992
OPUS Source: Kaiserslautern ; Saarbrücken : DFKI, 1992
SWD key words: Künstliche Intelligenz
DDC notations: 004 Computer science, internet
Publikation type: Report
Abstract: 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 to this record: urn:nbn:de:bsz:291-scidok-37849
Series name: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Series volume: 92-33
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_92_33.pdf11,88 MBAdobe PDFView/Open

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