de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Unification of terms with exponents

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44009

Socher-Ambrosius,  Rolf
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

MPI-I-93-217.pdf
(beliebiger Volltext), 105KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Socher-Ambrosius, R.(1993). Unification of terms with exponents (MPI-I-93-217). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-B456-6
Zusammenfassung
In an ICALP (1991) paper, H. Chen and J. Hsiang introduced a notion that allows for a finite representation of certain infinite sets of terms. These so called w-terms find an application in logic programming, where they can serve to represent finitely an infinite number of answers or to avoid nontermination in certain cases. Another application is in the field of equational logic. Using w-terms, it is possible to avoid a certain type of divergence of ordered completion. In all cases, unification is the basic computational aspect of this notation. Chen and Hsiang give a complete and terminating unification algorithm for w-terms. Recently, H. Comon introduced terms with exponents, thus significantly extending Chen and Hsiang's notion of w-terms. He provides a fairly complicated unification algorithm. This paper introduces a further syntactic generalization of Comon's notion together with a comparatively simple inference system for unification.