CS Seminar: Carla Piazza, April 18, 2000

Speaker

Carla Piazza,
Dipartimento di Matematica e Informatica, Università di Udine, Italy.

Date and Time

Tuesday, April 18, 2000 at 14:00

Place

Sala Riunioni,
Dipartimento di Matematica, Università di Parma, Via D'Azeglio 85/A, I-43100 Parma

Title

ACI1 Constraints

Abstract

Disunification is the problem of deciding satisfiability of a system of equations and disequations w.r.t. a given equational theory. In this talk we address the disunification problem in the context of ACI1 equational theories. This problem is of great importance, for instance, for the development of complex constraint solvers over sets. We start by providing a characterization of the interpretation structures suitable to model the axioms in ACI1 theories, and we develop extensions of (general) ACI1 which correspond to the "intuitive" Herbrand-based models on the class of conjunctions of equations and disequations. The satisfiability problem is solved using known techniques for the equality constraints and novel methodologies to transform disequation constraints into solved forms. We propose three solved forms, offering an increasingly more precise characterization of the set of solutions, and for each solved form we provide the corresponding rewriting algorithm. All the proposed solved forms are adequate to be efficiently used in the context of a Constraint Logic Programming system.

Contact Person

Gianfranco Rossi

[Page last updated on February 22, 2002, 15:16:33.]