CS Seminar: Carla Piazza, April 18, 2000
Dipartimento di Matematica e Informatica,
Università di Udine, Italy.
- Date and Time
Tuesday, April 18, 2000 at 14:00
Dipartimento di Matematica,
Università di Parma,
Via D'Azeglio 85/A,
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
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
[Page last updated on February 22, 2002, 15:16:33.]