Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Unification of terms with exponents

Socher-Ambrosius, Rolf

MPI-I-93-217. May 1993, 21 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-93-217.pdfMPI-I-93-217.pdfMPI-I-93-217.ps842 KBytes; 105 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Socher-Ambrosius, Rolf},
  TITLE = {Unification of terms with exponents},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-217},
  MONTH = {May},
  YEAR = {1993},
  ISSN = {0946-011X},