Incremental Constraint Satisfaction for Equational Logic Programming


María Alpuente, Moreno Falaschi and Giorgio Levi


In this paper we are concerned with an instance of the CLP scheme specialized in solving equations with respect to a Horn equational theory E. The intended structure H/E is given by the finest partition induced by E on the Herbrand Universe H over a finite one sorted alphabet. This work deals with the description of an incremental constraint solver as the kernel of an operational semantics for the language CLP(H/E). The primary issues are: how to verify the solvability of constraints in the structure H/E by using some sound and complete semantic unification procedure such as narrowing, how to simplify constraints in a computation sequence, how to achieve incrementality in the computation process and how to profit from finitely failed derivations as a heuristic for optimizing the algorithms.


Constraint logic programming, equational logic programming, term rewriting systems, equational unification, program semantics.