English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Report

Lazy unification with inductive simplification

MPS-Authors
/persons/resource/persons44582

Hanus,  Michael
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-93-215.pdf
(Any fulltext), 156KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Hanus, M.(1993). Lazy unification with inductive simplification (MPI-I-93-215). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B448-6
Abstract
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.