INCREMENTAL CONSTRAINT SATISFACTION FOR EQUATIONAL LOGIC PROGRAMMING

In this paper we are concerned with an instance of the Constraint Logic Programming (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.