From Model-Theoretic Algebra to Combined Constraint Satisfiability, Part I

modular method to decide constraint satisfiability relatively
to constraint theories which happens to be obtained as unions
of theories for which a decision algorithm for the same problem
is already available. However Nelson-Oppen methods suffers of
some drawbacks, the main of which is the limitation to disjoint
signatures. Despite the relevance of the problem, only little
progress has been made in the literature in order to overcome
this limitation. We propose a new approach based on classical
model-theoretic methods in Robinson's style.

The seminar is divided into two parts: in the first part we
basically review some standard material on model completeness,
by stressing both the original mathematical motivations and the
possibility of new applications in quite different contexts.
We also introduce the notion of $T_0$-compatibility which
generalizes the stable infiniteness requirement, thus giving
the main ingredient for our non-disjoint combination procedures.

In the second part, we analyze Nelson-Oppen procedure and show
how it naturally extends to the case of theories which are both
$T_0$-compatible with respect to a locally finite common
subtheory. We give some examples showing in particular how (old
and new) fusion decidability results in modal logic are instances
of our non-disjoint combination procedure. We finally drop the
local finiteness requirement when presenting applications to
saturation-based theorem proving.
Nelson-Oppen combination procedure provides a quite simple and
modular method to decide constraint satisfiability relatively
to constraint theories which happens to be obtained as unions
of theories for which a decision algorithm for the same problem
is already available. However Nelson-Oppen methods suffers of
some drawbacks, the main of which is the limitation to disjoint
signatures. Despite the relevance of the problem, only little
progress has been made in the literature in order to overcome
this limitation. We propose a new approach based on classical
model-theoretic methods in Robinson's style.

The seminar is divided into two parts: in the first part we
basically review some standard material on model completeness,
by stressing both the original mathematical motivations and the
possibility of new applications in quite different contexts.
We also introduce the notion of $T_0$-compatibility which
generalizes the stable infiniteness requirement, thus giving
the main ingredient for our non-disjoint combination procedures.

In the second part, we analyze Nelson-Oppen procedure and show
how it naturally extends to the case of theories which are both
$T_0$-compatible with respect to a locally finite common
subtheory. We give some examples showing in particular how (old
and new) fusion decidability results in modal logic are instances
of our non-disjoint combination procedure. We finally drop the
local finiteness requirement when presenting applications to
saturation-based theorem proving.