INCREMENTAL CONSTRAINT SATISFACTION FOR EQUATIONAL LOGIC PROGRAMMING

In this paper we are concerned with an instance of the Constraint Logi c Programming (CLP) scheme specialized in solving equations with respe ct 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 a n incremental constraint solver as the kernel of an operational semant ics for the language CLP(H/E). The primary issues are: how to verify t he 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 increm entality in the computation process and how to profit from finitely fa iled derivations as a heuristic for optimizing the algorithms.