Information Technology Reference
In-Depth Information
2
Preliminaries
2.1
Formulas
Let
Σ
R
be the usual real-based structure where the set of real numbers
is
associated with arithmetic operations, elementary functions and equality and
inequality relations. Formulas are written using a first-order language
L
defined
by an infinite countable set of variables
R
and a set of symbols with
arities, namely constants, functions and relations. In the following, we will use
the same symbols to denote the elements of
Σ
R
and the symbols of
L
.
A
term
is a syntactic expression built by induction from variables, constants
and function symbols of
L
.A
constraint
is an atomic formula of the form
fg
where
f
and
g
are terms and
is a relation symbol. A
formula
is defined by
induction from constraints, connectives and quantifiers. In the following, formu-
las will be written with the variables
x
1
,...,x
n
, the natural
n
being arbitrarily
large. Given a syntactic element
S
, the set of variables occurring in
S
is denoted
by Var(
S
), and the notation
S
(
x
1
,...,x
n
) will mean that the sets Var(
S
)and
{
{
x
1
,x
2
,...
}
are identical. The number of occurrences of any variable
x
i
in
S
will
be denoted by mult(
S, x
i
). Given two terms
f
and
g
and a term
h
occurring in
f
,let
f
[
h
x
1
,...,x
n
}
g
] denote the term obtained from
f
by replacing all the occurrences
of
h
with
g
.Let
←
be the set of terms.
Evaluating a term
f
(
x
1
,...,x
n
) in the domain
T
R
consists in assigning a
value
a
i
∈
R
to each variable
x
i
and applying the functions of
Σ
R
that corre-
spond to the symbols. The satisfaction of a constraint
C
(
x
1
,...,x
n
)requires
evaluating terms and verifying the relation. If the relation is verified then the
tuple (
a
1
,...,a
n
)isa
solution of
C
in the domain
R
.Let
f
R
and
C
R
respectively
n
to
denote the mapping from
R
R
corresponding to the evaluation of
f
and the
n
defined by the set of solutions of
C
in
relation of
.
A conjunction of constraints is a formula
F
(
x
1
,...,x
n
)oftheform
C
1
∧···∧
C
m
. The satisfaction of
F
consists in assigning a value
a
i
∈
R
R
R
to each variable
x
i
and verifying that all constraints
C
j
are satisfied. If the formula is satisfied
then the tuple (
a
1
,...,a
n
)isa
solution of
F
in the domain
R
.Let
F
R
denote the
n
relation of
. In the following, only
conjunctions of constraints will be considered, and a solution in
R
defined by the set of solutions of
F
in
R
R
will simply
be called
solution
.
2.2
Interval Arithmetic
Interval arithmetic [14,9] can be used to conservatively enclose the solutions of
formulas by Cartesian products of intervals. Interval computations are done in an
interval-based structure
Σ
I
. This structure can be defined by an homomorphism
µ
from
Σ
R
to
Σ
I
, as follows. The notations
f
R
,
C
R
and
F
R
used with the domain
R
will simply be changed into
f
I
,
C
I
and
F
I
.
Constants.
Consider the set of floating-point numbers
F
defined by the IEEE
standard [10] and the set of intervals
I
whose bounds are in
F
.Let[
I, I
]denote
Search WWH ::
Custom Search