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.

Authors

• María Alpuente
• Moreno Falaschi
• Giorgio Levi

Keywords

No keywords are indexed for this paper.