Summary: In a recent work, we have proposed a semantic framework for lazy functional logic programming with algebraic polymorphic types, i.e., polymorphic types whose data constructors must obey a finite set \({\mathcal C}\) of equational axioms. That framework included \({\mathcal C}\)-based rewriting calculi and a notion of model, proving soundness and completeness of \({\mathcal C}\)-based rewriting w.r.t. models, existence of free models for all programs and type preservation results, but no goal solving mechanism was presented. The present paper extends the previous one by developing a sound and complete procedure for goal solving, which is based on the combination of lazy narrowing with unification modulo \({\mathcal C}\). The resulting language is quite expressive for many kinds of problems, as e.g. action and change problems.
For the entire collection see [Zbl 0927.00043].