ACI1 constraints

Disunification is the problem of deciding satisfiability of a system of equations and disequations with respect to a given equational theory. In this paper we study the disunification problem in the context of ACI1 equational theories. This problem is of great importance, for instance, for the development of constraint solvers over sets. Its solution opens new possibilities for developing automatic tools for static analysis and software verification. In this work we provide a characterization of the interpretation structures suitable to model the axioms in ACI1 theories. The satisfiability problem is solved using known techniques for the equality constraints and novel methodologies to transform disequation constraints to manageable solved forms. We propose four solved forms, each offering an increasingly more precise description of the set of solutions. For each solved form we provide the corresponding rewriting algorithm and we study the time complexity of the transformation. Remarka...

• Type: Conference
• Year: 1999
• Where: AGP
• Authors: Agostino Dovier, Carla Piazza, Enrico Pontelli, Gianfranco Rossi
• Keywords: AGP 1999, Artificial Intelligence, Disunification Problems, Manageable Solved Forms, Solved Forms