SciDok

Eingang zum Volltext in SciDok

Lizenz

Report (Bericht) zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-37849
URL: http://scidok.sulb.uni-saarland.de/volltexte/2011/3784/


Unification theory

Baader, Franz

Quelle: (1992) Kaiserslautern ; Saarbrücken : DFKI, 1992
pdf-Format:
Dokument 1.pdf (11.883 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Künstliche Intelligenz
Institut: DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
DDC-Sachgruppe: Informatik
Dokumentart: Report (Bericht)
Schriftenreihe: Research report / Deutsches Forschungszentrum für Künstliche Intelligenz [ISSN 0946-008x]
Bandnummer: 92-33
Sprache: Englisch
Erstellungsjahr: 1992
Publikationsdatum: 01.07.2011
Kurzfassung auf Englisch: 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.
Lizenz: Standard-Veröffentlichungsvertrag

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English