
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,
I43100 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" Herbrandbased
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.]
