next.png up.png previous
Next: The language Up: Constraint Multiset Rewriting Previous: Constraint Multiset Rewriting


Constraint Systems

A constraint system is a tup.pngle $ {\mathscr C} =\langle {\mathscr V} ,$ $ {\mathscr L} ,$ $ {\mathscr D} ,$ $\mathscr{S},$ $\sqsubseteq^c\rangle$ where:
  1. $ {\mathscr V} $ is a denumerable set of variables;
  2. $ {\mathscr L} $ is a first-order language (the assertional language) defining a set of formulas with free variables in $ {\mathscr V} $ (the constraints), closed with respect to variable renaming, existential quantification and conjunction, and allowing equalities between variables;
  3. $ {\mathscr D} $ is a possibly infinite set (the interpretation domain);
  4. $\mathscr{S}({\varphi})$ is a set of mappings ${ {\mathscr V} }\rightarrow{ {\mathscr D} }$ (the set of solutions of a constraint $\varphi\in {\mathscr L} $) that preserves the usual semantics of equalities, $\wedge $ and $\exists$ (intersection and projection of the solutions);
  5. $\sqsubseteq^c$ is a relation such that $\varphi\sqsubseteq^c\psi$ implies $\mathscr{S}({\psi})\subseteq\mathscr{S}({\varphi})$ (the entailment relation: we say that $\psi$ entails $\varphi$).
We assume that $ {\mathscr L} $ contains constraints, denoted `$true$', and `$false$', which are identically true and identically false in $ {\mathscr D} $. By analogy with constraint programming, further requirements on constraint systems, like solution compactness [22], can be imposed. We refer to [22] for a discussion.


In the rest of the paper, we often denote the conjunction between constraints with a simple comma. We refer to a generic mapping $\sigma:{ {\mathscr V} }\rightarrow{ {\mathscr D} }$ as an evaluation for the variables in $ {\mathscr V} $. We use the notation $\langle {{x_1}\mapsto{d_1},{x_2}\mapsto{d_2},\ldots} \rangle $ to denote an evaluation $\sigma$ mapping $x_1$ to $d_1$, $x_2$ to $d_2$, and so on, and the notation ${\sigma}_{\vert{\vec{x}}}$ to denote the restriction of the evaluation $\sigma$ to the variables $\vec{x}$. We also say that a constraint $\varphi$ is satisfiable if $\mathscr{S}({\varphi})\not=\emptyset $.
\begin{example}
The class of {linear integer constraints} consists
of formula...
...is the usual entailment
relation for linear integer constraints.
\end{example}
Note that there exists several methods for checking satisfiability, entailment, and for variable elimination (see e.g. [10]) over linear arithmetic constraints.
\begin{example}
Let $\varphi$\ be $x>y\wedge x>z$, then
$\sigma=\langle {{x}\m...
...$(x>y)\sqsubseteq^c\varphi$, and
$\exists y.\varphi\equiv(x>z)$.
\end{example}
We are now ready to define the framework of multiset rewriting with constraints.
next.png up.png previous
Next: The language Up: Constraint Multiset Rewriting Previous: Constraint Multiset Rewriting
Giorgio Delzanno 2003-02-03