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


Lazy unification with inductive simplification

Hanus, Michael

MPI-I-93-215. March 1993, 20 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Unification in the presence of an equational theory is an important problem in theorem-proving and in the integration of functional and logic programming languages. This paper presents an improvement of the proposed lazy unification methods by incorporating simplification with inductive axioms into the unification process. Inductive simplification reduces the search space so that in some case infinite search spaces are reduced to finite ones. Consequently, more efficient unification algorithms can be achieved. We prove soundness and completeness of our method for equational theories represented by ground confluent and terminating rewrite systems.
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-215.pdfMPI-I-93-215.pdfMPI-I-93-215.dvi - MPI-I-93-215.dvi
96 KBytes; 156 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 = {Hanus, Michael},
  TITLE = {Lazy unification with inductive simplification},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-215},
  MONTH = {March},
  YEAR = {1993},
  ISSN = {0946-011X},