Next: The language
Up: Constraint Multiset Rewriting
Previous: Constraint Multiset Rewriting
Constraint Systems
A constraint system is a tup.pngle
where:
- is a denumerable set of variables;
- is a first-order language
(the assertional language) defining a set of
formulas with free variables in (the constraints),
closed with respect to variable
renaming, existential quantification and conjunction, and allowing
equalities between variables;
- is a possibly infinite set (the interpretation
domain);
-
is a set of mappings
(the
set of solutions of a constraint
) that preserves
the usual semantics of equalities, and
(intersection and projection of the solutions);
- is a relation such that
implies
(the entailment relation:
we say that entails ).
We assume that contains constraints, denoted `', and
`', which are identically true and identically false in
.
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
as an evaluation for the
variables in . We use the notation
to denote an
evaluation mapping to , to , and so
on, and the notation
to denote the
restriction of the evaluation to the variables
. We also say that a constraint is
satisfiable if
.
Note that there exists several methods for checking satisfiability, entailment, and for
variable elimination (see e.g. [10]) over linear arithmetic constraints.
We are now ready to define the framework of multiset rewriting
with constraints.
Next: The language
Up: Constraint Multiset Rewriting
Previous: Constraint Multiset Rewriting
Giorgio Delzanno
2003-02-03