# Incremental Constraint Satisfaction for Equational Logic Programming

### Author

María Alpuente, Moreno Falaschi and Giorgio Levi
### Abstract

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.
### Keywords

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