ACI1 constraints

10 years 7 months ago
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...
Agostino Dovier, Carla Piazza, Enrico Pontelli, Gi
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 1999
Where AGP
Authors Agostino Dovier, Carla Piazza, Enrico Pontelli, Gianfranco Rossi
Comments (0)