Analyses of Unsatisfiability for Equational Logic Programming


María Alpuente, Moreno Falaschi and Ferdinando Manzo


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.


Abstract interpretation, equational logic programming, term rewriting systems, universal unification.