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.