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 hdl:20.500.11880/25042 http://dx.doi.org/10.22028/D291-24986 |
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 | Size | Format | |
---|---|---|---|---|
RR_92_33.pdf | 11,88 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.