Author's Address

publication lies with the author. 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 unifica-tion 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 com-pleteness of our method for equational theories represented by ground confluent and terminating rewrite systems.