Analyses of Unsatisfiability for Equational Logic Programming
Author
María Alpuente, Moreno Falaschi and Ferdinando Manzo
Abstract
The problem of unifying pairs of terms with respect to an equational
theory (as well as detecting the unsatisfiability of a
system of equations) is in general undecidable. In this work we define a
framework based on abstract interpretation for the (static)
analysis of the unsatisfiability of equation sets. The main idea behind
the method is to abstract the process of semantic unification of
equation sets based on narrowing. The method consists of
building an {\it abstract narrower} for
equational theories and executing the sets of equations to be
detected for unsatisfiability in the approximated narrower. As an instance
of our framework we define a new analysis whose accuracy is enhanced by
some simple loop-checking technique.
This analysis can also be actively used for pruning the search tree of
an incremental equational constraint solver and can be integrated with
other methods in the literature. Standard methods are
shown to be an instance of our framework. To the best of our knowledge,
this is the first framework proposed for approximating equational
unification.
Keywords
Abstract interpretation, equational logic programming, term rewriting
systems, universal unification.