Convergent Approximate\\Solving of First-Order Constraints\\by Approximate Quantifiers
STEFAN RATSCHAN
Universit{\"a}t Linz
Exactly solving first-order constraints (i.e., first-order formulas over a certain predefined structure) can be a very hard, or even undecidable problem. In continuous structures like the real numbers it is promising to compute approximate solutions instead of exact ones. However, the quantifiers of the first-order predicate language are an obstacle to allowing approximations to arbitrary small error bounds. In this paper we remove this obstacle by modifying the first-order language and replacing the classical quantifiers with approximate quantifiers. These also have two additional advantages: First, they are tunable, in the sense that they allow the user to decide on the trade-off between precision and efficiency. Second, they introduce additional expressivity into the first-order language by allowing reasoning over the size of solution sets.
apprquantgen.tex



\documentclass[a4paper,11pt]{article}

\usepackage{ifthen}
\usepackage{psfig}
%\usepackage{transfig}
\usepackage{url}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{eepic}
%\usepackage{PCode}
\usepackage[all]{xy}
\usepackage{color}

\newcommand{\SetFigFont}[3]{\footnotesize} % deals with XFig bug 

\input{setup.tex}

%\input{thesis-defs.tex}

%felse(PLAIN,PLAIN,
%\newcommand{\qed}{\mbox{$\blacksquare$}}
%)
\newcommand{\SDen}{\mathbb{S}}
%\newcommand{\SEst}{\mathbb{E}}
\newcommand{\STrue}{\mathbf{T}}
\newcommand{\SFalse}{\mathbf{F}}
\newcommand{\SUVol}[1]{\mbox{UVol}(#1)}
\newcommand{\SExt}[1]{\mbox{Ext}_{#1}}
\newcommand{\SEncl}[1]{\mbox{Encl}(#1)}
%\newcommand{\SDescr}[1]{\mbox{Descr}(#1)}
%\newcommand{\SUndef}{\mathbf{U}}

\newcommand{\SIntL}[1]{\underline{#1}}
\newcommand{\SIntR}[1]{\overline{#1}}
\newcommand{\SInt}[1]{[\underline{#1}, \overline{#1}]}
\newcommand{\SPair}[1]{(\SIntL{#1},\SIntR{#1})}
\newcommand{\SPow}[1]{2^{#1}}

\newcommand{\SMG}{\SV^{*}}  % measure guess
\newcommand{\SQC}{\SQA^{*}} % quantifier choice
\newcommand{\SMGmin}[1]{\SIntL{\SV}^{*}_{#1}}
\newcommand{\SMGmax}[1]{\SIntR{\SV}^{*}_{#1}}
\newcommand{\SQCmin}[1]{\SIntL{\SQA}^{*}_{#1}}
\newcommand{\SQCmax}[1]{\SIntR{\SQA}^{*}_{#1}}

\newcommand{\SymDomain}{{\cal D}}
\newcommand{\SymSigmaAlg}{{\cal X}}
\newcommand{\SymSetDomain}{X}
\newcommand{\SymSetDomainAlt}{Y}
\newcommand{\SymBool}{{\cal B}}
%\newcommand{\SInterpr}{{\cal I}}
\newcommand{\SStruc}{{\cal S}}
\newcommand{\SVarAss}{\theta}
\newcommand{\SFInt}{\SStruc, \SVarAss, \SQC, \SMG} 
\newcommand{\SymTruthVal}{{t}}
%\newcommand{\SStrInt}{\SStruc, \SInterpr}
\newcommand{\SSA}[1]{{\cal #1}}
\newcommand{\SKAp}[1]{\Hat{#1}}
%\newcommand{\SCAp}[1]{\check{#1}}
\newcommand{\SBAp}[1]{\Tilde{#1}}
\newcommand{\SSubs}[3]{#1\frac{#2}{#3}}

\newcommand{\lsem}{[\![}
\newcommand{\rsem}{]\!]}
\newcommand{\SBIS}[2]{\lsem{#1},{#2}\rsem}   
\newcommand{\SBI}[1]{\SBIS{\underline{#1}}{\overline{#1}}}   % biinterval
\newcommand{\SQA}{q}
\newcommand{\SV}{\mu}
\newcommand{\SSS}{d}






\title{Convergent Approximate\\Solving of First-Order Constraints\\by Approximate Quantifiers}

\author{STEFAN RATSCHAN\\Research Institute for Symbolic Computation\\
Universit{\"a}t Linz}




\begin{document}



\maketitle

\begin{abstract}
  Exactly solving first-order constraints (i.e., first-order formulas over a certain
  predefined structure) can be a very hard, or even undecidable problem. In continuous
  structures like the real numbers it is promising to compute approximate solutions
  instead of exact ones.  However, the quantifiers of the first-order predicate language
  are an obstacle to allowing approximations to arbitrary small error bounds.  In this
  paper we remove this obstacle by modifying the first-order language and replacing the
  classical quantifiers with approximate quantifiers.  These also have two additional
  advantages: First, they are tunable, in the sense that they allow the user to decide on
  the trade-off between precision and efficiency.  Second, they introduce additional
  expressivity into the first-order language by allowing reasoning over the size of
  solution sets.
\end{abstract}







\section{Introduction}

%\paragraph{Problem}
Solving first-order constraints, (i.e., first-order formulas over a
certain predefined structure), and especially first-order constraints over the reals. 
has numerous
applications~\cite{Ratschan:01e,Dorato:95,Benhamou:00a,Dolzmann:97,Hong:97,Jirstrand:96}.
% Solving such constraints usually means to find a representation of their solution set that
% is in some sense simple. 
% For example, the method of quantifier elimination takes a
% first-order constraint and returns an equivalent, but quantifier-free constraint. Such
% quantifier elimination methods exist for real first-order constraints containing only the
% predicate symbols $=$, $\leq$ and $<$, the function symbols $+$ and $.$, and rational
% constants (i.e., the theory of real-closed fields~\cite{Tarski:51}). 
However, solving such constraints over the reals is either highly complex (e.g.,
when considering the predicate symbols $=$ and $\leq$, and the function symbols $+$ and
$\times$~\cite{Tarski:51,Fischer:74,Davenport:88,Weispfenning:88}), or
impossible~\cite{Tarski:51,Richardson:68}.
% But as soon as one
% adds functions like $\sin$ to the theory, the problem becomes undecidable.  Even when
% restricting one-selves to the theory of real-closed fields, quantifier elimination is
% usually extremely complex and complicated.
%\paragraph{Solution: approximate quants}
To deal with this problem, one can either restrict one-selves to more special problem
classes (see e.g.~\cite{Weispfenning:94,Hong:93a,GonzalezVega:96}), or relax the problem
by allowing approximation up to a user-specified error bound (as proposed by
H.~Hong~\cite{Hong:95c}). This paper studies the general feasibility of the second
approach. Its main contributions are: To show that even for this relaxed specification
we might have to do exact intermediate computation; and to introduce a modification of the
first-order predicate language---approximate quantifiers---for which this problem does
not occur. 

% In an earlier paper \cite{Ratschan:00}, we have shown how one can compute an approximate
% solution set of a constraint by taking approximations of the identity functions denoted by
% the variables and propagating them over the structure of the constraint.  In this paper
% we additionally require that the error of the resulting approximation is smaller than a
% user-specified positive real bound $\varepsilon$. We show that for constraints containing
% quantifiers this is in general not possible. We solve this problem by introducing new,
% approximate quantifiers.

These quantifiers have two additional advantages: First, they are tunable, in the sense
that they allow the user to decide on the trade-off between precision and efficiency.
Second, they introduce additional expressivity into the first-order predicate language, by
allowing reasoning over the size of solution sets.

%\paragraph{Annotation with one real}
The first step to introduce approximate quantifiers is to allow quantifiers with a
positive real annotation $\SQA$, with the intuitive meaning that a formula
$\exists_{\SQA} x\;\phi$ is true iff the volume of the solution set of $\phi$ is
greater than $\SQA$. We will see that this does not yet allow the computation of
approximate solution sets up to arbitrarily small, user-specified, error bounds.

%\paragraph{Idea for approximate quantifiers}
So we allow quantifiers to be annotated with a real interval $\SInt{\SQA}$, with the
intuitive meaning that the exact annotation can be any element of $\SInt{\SQA}$. This
allows an algorithm to choose the most suitable value in $\SInt{\SQA}$ and we do not
  care which one. This means that a sentence in the language does not have one distinct
truth-value but has a set of possible truth-values~(cmp.  with~\cite{Hehner:84}
or~\cite{Hoare:98}). We will prove that, from a good enough approximation of the solution
sets of the atomic sub-constraints, we can always compute at least one of these
truth-values, and thus one can always attain an arbitrarily small error bound when
computing approximate solution sets.

%Then we do not compute \emph{the} truth-value but only \emph{a} possible
%truth-value of a sentence.

%\paragraph{Unmeasurable sets}
% Now the problem arises that sometimes one cannot assign a volume to every solution set,
% because it might be unmeasurable~(see any book on measure theory \cite{Halmos:50,Bauer:90}
% for details).  Furthermore it might be interesting to deliberately use less powerful
% measures, for example a floating point box measure that models the sets that can be
% measured by floating point boxes on a computer. Every unmeasurable set has several
% possible volumes between the inner and outer measure, but we \emph{don't know} which one.

%\paragraph{Method for approximate quantifiers}
Following the usual approach (see e.g.~\cite{Walicki:97}), one would implement such a
logic using sets of truth-values (representing a many-valued logic~\cite{Urquhart:86,Rescher:69})
instead of single truth-values. We show that this approach is not suitable here and
present a new method that is completely orthogonal to the semantics usually given to
formulas when we do not know the value of certain predicate and function symbols and
thus assign validity to the formula using all possible predicate and function symbol
assignments (i.e., interpretations). Although arising from problems over real numbers, the
resulting first-order language is completely domain-independent.

%\paragraph{Nondeterminism}
The above situation that there are several possible values for an object, and we either do
not know or do not care which one should be taken, is commonly called \emph{don't know}
and \emph{don't care nondeterminism}, respectively. Here both forms occur at the same
time, which creates various difficulties through their interaction. Our approach gives
general insight into such a situation by showing how one can compute with such
nondeterministic objects, nevertheless. So our language can be easily extended to take
into account nondeterminism coming from other sources. For example uncertain coefficients
of occurring polynomials can be either modeled as don't care nondeterminism (the
\emph{united} approach) or as don't know nondeterminism (the \emph{robust}
approach)~\cite{Bouchon-Meunier:96,Gardenes:01,Shary:96}.

%\paragraph{Paper Structure}
The structure of the paper is as follows: In Section~\ref{sec:appr-constr-solv}, we give
the specification of solving first-order constraints approximately up to some
user-specified error bound, and informally show that this is impossible for constraints
containing classical quantifiers.  In Section~\ref{sec:model-appr-comp}, we develop a
suitable formal model for approximate computation. In Section~\ref{sec:prop-appr-solut}
use this model to formalize the approximate solving of first-order constraints and its problems discussed in
Section~\ref{sec:appr-constr-solv}.
In Section~\ref{chp:quant}, we give a
first-order language where the classical quantifiers are replaced by approximate ones.  In
Section~\ref{sec:appr-comp-appr}, we apply the formal model for approximately solving
first-order constraints to approximate quantifiers. In Section~\ref{sec:repr-appr-solut},
we show how to deal with the resulting two forms of nondeterminism. In
Section~\ref{sec:biappr-proj-conv}, we prove that one can solve constraints that contain
approximate instead of classical quantifiers up to an arbitrary small error bound. In
Section~\ref{sec:related-work}, we discuss related work, and in
Section~\ref{sec:conclusion}, we give a final conclusion.

\section{Approximate Solving of First-Order Constraints}
\label{sec:appr-constr-solv}

%\paragraph{Why Approximation}
%Here ``simple representation'' informally means that such a representation
%makes it easy to test, whether some real number tuple is an element of the set.

Throughout the paper we use the term ``constraint'' as a shortcut for ``first-order
constraint'', that is, a first-order formula over a certain, predefined structure
$\SStruc$.  We fix a set $V$ of variables and define a \emph{variable assignment} as a
function from $V$ to $\SStruc$. For a variable assignment $\SVarAss$, an element
$a\in\SStruc$, and variable $v\in V$, $\SSubs{\SVarAss}{a}{v}$ is the variable assignment
that is the same as $\SVarAss$ except that it assigns $a$ to $v$.

We define the property that a constraint \emph{is true} for a certain variable assignment
(or \emph{is satisfied by it}) as usual.  A \emph{potential solution set} is a set of
variable assignments (we use the adjective ``potential'' for signifying the
independence from a specific constraint), and the \emph{solution set of a first-order constraint
  $\phi$} is the set of variable assignments for which $\phi$ is true

Sometimes we denote the solution set of a
closed first-order constraint (i.e., \emph{sentence}) by the Boolean constant $\STrue$
(which represents the set of all variable assignments), or $\SFalse$ (which represents the
empty set). In this case we also speak of the \emph{truth-value} (instead of solution set)
of a first-order constraint.

Recall that the notion of volume is modeled in mathematics by measure spaces (see any
textbook on measure theory, for example~\cite{Halmos:50}, for details).  For any measure
$\SV$ and set $A$, the inner measure $\SIntL{\SV}(A)$ is the supremum of the measures of
all measurable subsets of $A$ (or $-\infty$, if this supremum does not exist), and the
outer measure $\SIntR{\SV}(A)$ is the infimum of the measures of all measurable supersets
of $A$ (or $\infty$, if this infimum does not exist). For any set $A$,
$\SIntL{\SV}(A)\leq\SIntR{\SV}(A)$. If $A$ is measurable, then
$\SV(A)=\SIntL{\SV}(A)=\SIntR{\SV}(A)$---in this case we often use the term \emph{volume}
for measure. Furthermore, we call a function $\SV$ \emph{possible measure} iff for any set
$A$, $\SV(A)\in [\SIntL{\SV}(A),\SIntR{\SV}(A)]$.  We straightforwardly extend any measure
on $\SStruc^{|V|}$ to a measure on (potential) solution sets by measuring the tuples corresponding to
the variable assignments in the (potential) solution set.

We want to solve constraints: Given some constraint, we want to get a simple (e.g.,
quantifier-free) representation of its solution set.
% However, for the structure of real numbers, we cannot represent
% arbitrary elements on computers, so we also cannot represent arbitrary solution sets.
% Methods for solving real first-constraints exactly exist only for special cases (e.g., for
% the theory of real-closed fields, which allows only the function symbols $+$ and
% $.$~\cite{Collins:75,Tarski:51}).  But even in these special cases the methods usually
% have huge complexity~\cite{Davenport:88,Weispfenning:88}, and often create output that is
% too complicated for practical use.
%\paragraph{Algorithm Specification}
However, over the real numbers, this problem is either highly
complex~\cite{Tarski:51,Fischer:74,Davenport:88,Weispfenning:88} or
undecidable~\cite{Tarski:51,Richardson:68}.  So we can only hope to tackle the general
problem, if we relax it.  As proposed by H.~Hong~\cite{Hong:95c}, we do this by
allowing approximation. This results in the problem specification of
Figure~\ref{fig:spec}.

\begin{figure}[htbp]
\begin{given-find}{
A constraint $\phi$, and\\
a positive real error bound $\varepsilon$}{
Sets $Y$ and $N$ of variable assignments, such that\\
    $\phi$ is true for all elements of $Y$,\\
    $\phi$ is false for all elements of $N$,\\
    the volume of the variable assignments not in $Y$ or $N$ is smaller than $\varepsilon$
}\end{given-find}
   
    \caption{Problem Specification}
    \label{fig:spec}
\end{figure}

%\paragraph{Computing the Specification}
In this paper we assume that we already have an algorithm that implements this
specification for atomic input constraints. For example, one can use for this a
branch-and-bound approach based on interval arithmetic~\cite{Jaulin:01b}. In theory, one
would need arbitrary precision here. In practice, however, fast 
machine-precision floating-point arithmetic usually suffices.

We would like to find an algorithm that fulfills the given specification based on such a
solver for atomic constraints.  However, this is impossible in general, because sometimes
exact solution sets of atomic sub-constraints are needed to compute such approximate
solutions. We show this here informally and formalize the arguments in the two following
sections.
% We do all our considerations for existential
% quantification only. They can be easily adapted to the dual case of universal
% quantification.
%
% Assume that we can compute approximations of solution sets of atomic constraints up to
% arbitrarily small positive error bounds. This information is not enough for fulfilling the
% preceding input/output specification for computing approximate solution sets of quantified
% constraints.
%
Take an input constraint of the form $\exists x\;\phi$ without free variables, where
$\phi$ is an atomic constraint with an empty solution set. Determine for all $x$, except
for a set of arbitrarily small but positive volume, whether $x$ is in the solution set of
$\phi$. From this information we cannot deduce that $\exists x\;\phi$ is false, because
some of the remaining $x$ might be in the solution set of $\phi$, in which case $\exists
x\;\phi$ would be true.

One could suspect that the reason for this problem is, that a classical quantifier has to
take into account arbitrarily small solution sets of the quantified sub-constraint. So let
us introduce an additional quantifier $\exists_{\SQA}$ (the \emph{existential volume
  quantifier}) into the first-order predicate language, where $\SQA$ is a non-negative
real number. A closed constraint of the form $\exists_{\SQA} x\;\phi$ is true iff the
volume of the $x$, for which $\phi$ is true, is greater than $\SQA$. But even for this
quantifier, we have the same problem: Take an input constraint of the form
$\exists_{\SQA} x\;\phi$.  Assume that the solution set of $\phi$ has exactly the volume
$\SQA$.  Determine for all $x$, except for a set of arbitrarily small but positive volume,
whether $x$ is in the solution set of $\phi$.  Again, from this information we cannot
deduce whether $\exists_{\SQA} x\;\phi$ is true.  Note that one can easily find
examples of constraints \emph{with} free variables, that show the same behavior; in this
case we can deduce for no element of the free-variable space whether it is an element of
the solution set of such a constraint.

Speaking in the language of numerical analysis, the problem of finding approximations of
solution sets of quantified constraints is \emph{ill-posed} for certain inputs.  This
means that one can only solve it by approximation methods either after using more
information, or after relaxing the problem.  Following the latter approach, we introduce
different quantifiers, for which the problem does not occur.

\section{A Model for Approximate Computation}
\label{sec:model-appr-comp}

Before solving the problems described in the last section, we formalize them. For this we
develop a model for approximate computation in this section, and apply it to approximate
solving of first-order constraints in the next section. Readers who want to
see a solution to the problem immediately, without being interested in formal proofs, can
skip these sections and can directly jump to Section~\ref{chp:quant}.

Assume a set $A$. Instead of doing exact computation in $A$, we use a set $\SKAp{A}$ for
approximating computation in $A$. For this we add a notion of error, that is, a function
from $\SKAp{A}$ to $\mathbb{R}^{+}$.  For example, one can do approximate computation for
the real numbers using the set of rational intervals. Here the error of an interval is its
width. Take the expression $2x+1$. If we know that $x$ is in the interval $[2,3]$ then we
can deduce that the value of the expression is within $[5, 7]$---a result with error $2$.

Here we would like to be able to make the output error arbitrarily small by making the input
error small:

\begin{definition}
\label{def:convergent}
  A function $f: \SKAp{A}\rightarrow \SKAp{A}$ is \emph{convergent} iff 
    for all $\varepsilon\in\mathbb{R}^{+}$
      there is a $\delta\in\mathbb{R}^{+}$ such that
        for all $\SKAp{a}\in\SKAp{A}$ such that the error of $\SKAp{a}$ is less or equal $\delta$,
          the error of $f(\SKAp{a})$ is less or equal $\varepsilon$.
\end{definition}

Note that this definition corresponds to the definition of uniform continuity in analysis;
this notion and similar ones are used as necessary conditions for computability in
effective analysis~\cite{Bishop:67,Bishop:85,Pour-El:89,Weihrauch:00}.

We assume that every element $\SKAp{a}\in\SKAp{A}$ gives us the information that the
result of some computation is in a certain subset of $A$.  So we use subsets of $A$ for
modeling approximate computation from now on and simply identify $\SKAp{A}$ with
$\SPow{A}$. As in the example of rational intervals, very often one just uses certain
subsets of $A$ that allow a convenient representation.

Observe that it can also occur that we cannot define a certain function exactly, but only
approximately. This means that there are several possible functions, and we do not know
which one is the correct one to use. Again we represent this \emph{don't know}
nondeterminism by a set of functions, which we call \emph{approximate function}. For
example, the function computing the weight of a certain mass depends on the constant
describing gravitational acceleration. The exact value of this constant depends on the
distance from the center of the earth, and so we have not exact value for it---only an
interval covering all its possible values on the surface of the earth. Therefore
several such functions are possible and the whole function is approximate.

If we want to do approximate computation, then the best possible result we can obtain
without producing wrong results, is:

\begin{definition}
  For an approximate function $\SKAp{f}$ such that each element is a function on $A$, for
  an $\SKAp{a}\in\SKAp{A}$
  \[ \SExt{\SKAp{f}}(\SKAp{a}):= \{ f(a)\:|\: f\in\SKAp{f}, a\in\SKAp{a} \} \] 
We call $\SExt{\SKAp{f}}$ the \emph{extension of $\SKAp{f}$}.
\end{definition}

For example, interval arithmetic~\cite{Moore:66,Neumaier:90} defines approximate
computation on the real numbers in this way. However, instead of computing with exact
rational end-points, the results are usually rounded to the smallest super-interval whose
end-points are floating-point numbers.

Clearly the fact that the extension of a function is not convergent, implies that we cannot
use approximate computation to compute this function up to an arbitrarily small error.

\section{Approximate Computation and Classical Quantifiers}
\label{sec:prop-appr-solut}

%\paragraph{Approximate Solution Sets}

Now we use the tools developed in the last section to show that classical quantifiers are
an obstacle to approximate computation. Let $\SDen$ be the set of potential solution sets. Then we
can do approximate computation using $\SKAp{\SDen}$, whose elements we call
\emph{potential approximate solution sets}, where the \emph{approximate solution set of a constraint
  $\phi$} is a potential approximate solution set that contains the solution set of $\phi$.


% In order to being able apply
% Definition~\ref{def:convergent}, we define some measure space on solution sets.

% \begin{definition}
% \label{def:apprSolSet}
% For any first-order constraint $\phi$, an \emph{approximate solution set} of $\phi$ is a
% set of solution sets that contains the solution set of $\phi$.
% \end{definition}

% In the following we will model approximate computation by sets of possible values on which
% we define the error as its volume 


% For reasons that will become clear later we introduce
% nondeterminism for functions also, and call a set of functions \emph{approximate
%   function}.

%\paragraph{Spec. from Approximate Solution Sets}
We can deduce the information we want to find for our specification
(Figure~\ref{fig:spec}) as follows:

\begin{definition}
  A variable assignment $\SVarAss$ is \emph{determined to true} by a potential
  approximate solution set $\SKAp{d}$ iff for all $d\in\SKAp{d}$, $\SVarAss\in d$. It is
  \emph{determined to false} by $\SKAp{d}$ iff for all $d\in\SKAp{d}$, $\SVarAss\not\in d$.  It
  is \emph{determined} by $\SKAp{d}$ iff it is either determined to true or determined to
  false by $\SKAp{d}$.
\end{definition}

Now we can easily define the error of a potential approximate solution set $\SKAp{d}$ as
the upper measure of the set of all variable assignments that are not determined by
$\SKAp{d}$.

For example, an approximate solution set of the constraint $x^2+y^2\leq 1$ might contain
all the potential solution sets that do not contain elements outside of the rectangle
$[-1,1]\times[-1, 1]$ (the solution set of $x^2+y^2\leq 1$ is one of these). In this case
all variable assignments assigning values outside of $[-1, 1]$ are determined to false,
and no variable assignment is determined to true. By measuring the size of the rectangle $[-1,
1]\times[-1, 1]$ we get the error $4$ of this approximate solution set.

%We adopt the convention that in $\mathbb{R}^{0}$ the volume of the empty set is zero and the
%volume of the set containing the empty tuple is infinite. 

%\paragraph{Classical Projection Operator}

For a constraint of the form $L(\phi_{1},\dots,\phi_{n})$, where $L$ is either a
quantifier and a variable (in this case $n=1$) or a connective, the solution set of the
total constraint is a function of the solution sets of the sub-constraints
$\phi_{1},\dots,\phi_{n}$. It is easy to show that the functions corresponding to
connectives are convergent in the sense of Definition~\ref{def:convergent}. So we will
concentrate on the case where $L$ contains an (existential) quantifier. In this case we have the
following function on potential solution sets (see~\cite{Ratschan:00} for the other
cases).

\begin{definition}
  For a variable $v\in V$, the \emph{$v$-projection operator} is a function $P$ on
  potential solution sets such that a variable assignment $\SVarAss\in P(d)$ iff there is
  an $a\in\SStruc$ such that $\SSubs{\SVarAss}{a}{v}\in d$.
\end{definition}

%%\paragraph{Equivalence: Proj. Op. vs. Logic}
% Then for every solution set $d$ of a constraint $\phi$, $P(d)$ is the solution set of the
% constraint $(\exists x)\phi$. Now we want to apply the projection operator to approximate
% information:

%\paragraph{Extension of Function to Approximate Solution Sets}
%In a similar way, approximations of the solution sets of the sub-constraints determine an
%approximation of the solution set of the whole constraint.

%\paragraph{Equivalence: Extension of Proj. Op. vs. Logic}
So, for a constraint $\exists x\;\phi$, we can compute an approximate solution set of the
total constraint from an approximate solution set of $\phi$, by applying $\SExt{\{ P \}}$,
where $P$ is the $x$-projection operator, to the approximate solution set of $\phi$.
Extending the above example to the constraint $\exists y\; x^2+y^2\leq 1$, we can use the
$y$-projection operator to compute an approximate solution set of this constraint. The
result contains all potential solution sets that do not assign values less than $-1$ or
greater than $1$ to $x$. This determines all variable assignments for which $x$ is not in
$[-1, 1]$ to false, and leaves all other variable assignments undetermined.

%\paragraph{Usability for Approximate Computation}
Using the argument from Section~\ref{sec:appr-constr-solv} it is easy to show that the
extension of the approximate function that contains the projection operator is not
convergent. Thus we cannot fulfill our specification (Figure~\ref{fig:spec}) for
constraints containing quantifiers. So we have to find a similar, but easier problem for
which we can fulfill the specification. We do this by introducing quantifiers that
approximate classical quantification, but result in a convergent projection operator.

\section{A First-Order Predicate Language with Approximate Quantifiers}
\label{chp:quant}

%\paragraph{Preliminaries: Measure Space}
%Since we do not confine ourselves to the domain of real numbers, in this section we speak of formulas and
%sentences instead of constraints.  

%\paragraph{Reason: Discontinuity}
Classical quantifiers and volume quantifiers do not allow approximation up to an
arbitrarily small error bound because they discontinuously change from false to true. If
the size of the solution set of the quantified constraint is exactly at this point of
discontinuous change, then we cannot decide between true and false using approximate
computation.

%\paragraph{How to Avoid Discontinuity}
We avoid this discontinuous change by using volume quantifiers $\exists_{\SQA}$
($\forall_{\SQA}$) for which we do not specify the annotation $\SQA$ exactly, but only
require it to be within a certain interval $\SInt{\SQA}$.  Then a constraint solver can
choose an element of this interval element for which it can safely decide whether the
total constraint is true, using the available approximate information. This means that
sentences containing such an approximate quantifier can possibly be both true and
false---depending on which element of the interval $\SInt{\SQA}$ we choose. This happens
if the size of the solution set of a quantified constraint is within the interval $\SInt{\SQA}$ (see
Figure~\ref{fig:apprQuant}).

\begin{figure}[htbp]
  \begin{center}
    \input{uncont.pstex_t}
    \caption{Approximate Quantifiers}
    \label{fig:apprQuant}
  \end{center}
\end{figure}

%\paragraph{Dual Nondeterminism to Approximate Solution Set}
Recall that an approximate solution set of a constraint consists of several potential
solution sets, and we do not know which of them is the correct one---we have \emph{don't
  know} nondeterminism.  But here we are in exactly the dual situation: We allow several
equally possible truth-values, and we do not care, which of them is chosen---thus we
have \emph{don't care} nondeterminism.

%\paragraph{Unmeasurable Solution Sets}
Since our quantifiers depend on the size of the solution set of the quantified constraint,
we also have to deal with the situation when this solution set is not measurable.
Fortunately, this again is \emph{don't know} nondeterminism. If the solution set is not
measurable, then we only know that its volume is between the inner and the outer measure,
but we do not know which of these.

%\paragraph{Naive Approach: Many-Valued Logic}
A naive approach to modeling such a situation, where a logical formula can have more than
one solution set, would propagate sets of truth-values by applying the logical symbols
element-wise.  For example, if for a sentence $\phi_{1}\wedge\phi_{2}$ the approximate
truth-value of $\phi_{1}$ is $\{\STrue\}$ and the approximate truth-value of $\phi_{2}$
is $\{\STrue,\SFalse\}$ then the combination of all these elements yields a truth-value
of $\{\STrue,\SFalse\}$ for the whole sentence.  This results in a many-valued
logic~\cite{Urquhart:86,Rescher:69}.  In order to show that this approach is not feasible,
we first demonstrate, that this would need a more complicated many-valued logic, and then
give a reason, why to avoid many-valued logics altogether:

One would need a more complicated many-valued logic, because of the need to consider the
interaction between the \emph{don't care} nondeterminism resulting from the approximate
quantifiers and the \emph{don't know} nondeterminism resulting from unmeasurable sets.
Approximate quantifiers can result in an approximate truth-value $\{ \STrue, \SFalse \}$.
An unmeasurable solution set can result in an unknown solution set of a formula.
Typically one would model this by an empty set.  But one wants to be able to assign the
approximate truth-value $\{\SFalse\}$ to the whole formula $\phi_{1}\wedge\phi_{2}$, if
$\phi_{1}$ has the approximate truth-value $\{\SFalse\}$ and $\phi_{2}$ has the empty
approximate solution set, although element-wise combination yields the empty set in this
case. This problem arises because a non-existing truth-value for $\phi_{2}$ means that it
can have two possible truth-values ($\STrue$ or $\SFalse$).  We do not know which one, but
we have modeled only the \emph{don't care} form of nondeterminism.

One could construct a many-valued logic that solves this
problem~\cite{Ginsberg:88,Fitting:91}, but there
is another problem that makes us avoid such an approach altogether: For example, consider
$\phi\wedge\neg\phi$, where $\phi$ has the approximate solution set $\{ \STrue, \SFalse
\}$. Then element-wise combination yields the approximate solution set $\{ \STrue,
\SFalse\}$, although we want this formula to be false in any case. The reason is, that a
many-valued logic forgets the information about the equality of $\phi$ in both branches of
$\wedge$~\cite{Urquhart:86,Rescher:69}. This also makes it impossible to define
$\leftrightarrow$ (equivalence) as an abbreviation. A similar problem also occurs in
interval mathematics~\cite{Moore:66,Neumaier:90}, where the information about equal terms
is lost.

%\paragraph{Syntax}
Before going into the details of our solution, we fix the syntax of the new language.  It
is the usual one of the first-order predicate language, with the only exception that
instead of classical quantifiers, approximate quantifiers are used.  Consider the example
$\forall^{1}_{[0.1, 0.2]} x\;\exists^{2}_{[0.0, 0.1]} y\; [\;x>0 \wedge y=0\;]$.  The
quantifiers have a subscript consisting of a nonnegative real interval (the
\emph{annotation}).  Furthermore they have a positive integer superscript (the
\emph{tag}). We require that, within a formula,
quantifiers that have the same tag, also have the same annotation.

Tag equality indicates equal (nondeterministic) behavior of the according quantifiers.
That is, for quantifiers that have the same tag, the same element of the corresponding annotations
should always be chosen. This will allow us to make $A\wedge\neg A$ false in any case, and
makes the definition of $A\leftrightarrow B$ as an abbreviation for $(A\vee\neg B) \wedge
(\neg A\vee B)$ possible.
%Furthermore we allow parallel quantification over
%more than one variable. Parallel quantification over a tuple $(v_{1},\dots,v_{n})$ will be
%semantically different from sequential quantification over the single variables $v_{i}$.

If the annotation of a quantifier is a one-element interval then we say that the
quantifier is \emph{deterministic}. A formula where all the tags of quantifiers that
are not deterministic, are different, is called \emph{free}. Often we do not explicitly
write down the tags but assume an arbitrary tagging such that a formula is free.

%\paragraph{Semantics}
For assigning semantics to such formulas, we need to extend some of the usual definitions of the
first-order predicate logic:

\begin{definition}
  An \emph{m-structure} consists of a measure space $\SymDomain$, and for each relation and
  function symbol an according relation and function in $\SymDomain$. 
\end{definition}

% \begin{definition}
%   An interpretation $\SInterpr$ in a structure $\SStruc$ assigns to every $n$-ary
%   predicate symbol an $n$-ary relation in $\SStruc$, and to every $n$-ary function symbol
%   an $n$-ary function in $\SStruc$.
% \end{definition}

As usual, by abuse of notation, we denote by $\SymDomain$ also the set on which the
measure space is defined.  %We call it the \emph{domain} of the structure.  
Terms can be
interpreted as usual in m-structures. We again fix an arbitrary m-structure $\SStruc$ with
measure space $\SymDomain$ that defines a measure $\SV$. For defining the semantics of approximate
quantification we use a method that is completely orthogonal to the semantics usually
given to formulas when we \emph{don't know} the value of certain predicate and function
symbols and thus assign validity to the formula using all possible predicate and function
symbol assignments.

It is straightforward to give semantics to a first-order constraint with approximate
quantifiers if we already know for each occurring quantifier with annotation
$\SInt{\SQA}$, which volume quantifier $\exists_{\SQA}$ or $\forall_{\SQA}$, where
$\SQA\in\SInt{\SQA}$, and which possible measure to use.  So, in analogy to the notion of
structure which assigns information to predicate and function symbols, we assign
information to quantifiers as follows:

\begin{definition}
  Given a first-order constraint $\phi$, a function $\SQC:
  \mathbb{N}\rightarrow\mathbb{R}$ is a \emph{quantifier choice for $\phi$} iff for every
  $t\in\mathbb{N}$ that occurs as a quantifier tag in $\phi$, $\SQC(t)\in [\SIntL{\SQA},
  \SIntR{\SQA}]$, where $[\SIntL{\SQA}, \SIntR{\SQA}]$ is the annotation of the
  quantifiers occurring in $\phi$ that are tagged by $t$.
\end{definition}

In a similar way, we can assign to each tag the possible measure that should be used
(recall from Section~\ref{sec:appr-constr-solv} that in the case of measurable sets a
possible measure just assigns its measure, otherwise any value between the inner and the
outer measure).

\begin{definition}
  A \emph{measure guess} is a function \[\SMG: \mathbb{N}\rightarrow (2^{\SymDomain}\rightarrow [0, \infty]),\] such that for all $t\in\mathbb{N}$,
  $\SMG(t)$ is a possible measure.
\end{definition}

It is an easy exercise to define the solution set of a constraint $\phi$, for a certain
quantifier choice $\SQC$ for $\phi$, and a certain measure-guess $\SMG$. Now we model that
we \emph{don't care} for the quantifier choices and \emph{don't know} about the right
measure guesses. For this we introduce two notions corresponding to the notion that a
constraint is true. The essence is, that now different quantifier choices can be used, and
each choice can result in a different overall result:

\begin{definition}
\label{def:truthVal}
A first-order constraint $\phi$ \emph{is true} for a variable assignment $\SVarAss$ iff
there is a quantifier-choice $\SQA^{*}$ for $\phi$, such that for all measure-guesses
$\SV^{*}$, $\phi$ is true for $\SVarAss$, $\SQA^{*}$, and $\SV^{*}$.  A
first-order constraint $\phi$ \emph{is false} for a variable assignment $\SVarAss$ iff
there is a quantifier-choice $\SQA^{*}$ for $\phi$, such that for all measure-guesses
$\SV^{*}$, $\phi$ is not true for $\SVarAss$, $\SQA^{*}$, and $\SV^{*}$.
\end{definition}

As an example assume a sentence $\exists_{\SInt{\SQA}} x\;\phi$, where $\phi$ has a
measurable solution set $d_{\phi}$. If the volume of $d_{\phi}$ is less or equal
$\SIntL{\SQA}$ the constraint is false; if the volume of $d_{\phi}$ is greater than
$\SIntR{\SQA}$, then $\phi$ is true; but if the volume of $d_{\phi}$ is within
$\SInt{\SQA}$, $\phi$ is both true and false. So we have exactly the behavior sketched in
Figure~\ref{fig:apprQuant}.

% truth-values obtained by this definition cannot be propagated as usual. For example, if
% $\SymTruthVal$ is a truth-value of $\phi_{1}\vee\phi_{2}$ then there are not necessarily
% truth-values $\SymTruthVal_{1}$ of $\phi_{1}$ and $\SymTruthVal_{2}$ of $\phi_{2}$ such
% that $\SymTruthVal=\SymTruthVal_{1}\vee\SymTruthVal_{2}$. For example if $\phi_{1}$ is
% true, then $\phi_{1}\vee\phi_{2}$ is true even if there is no truth-value of $\phi_{2}$.

% Since we are interested in solving formulas instead of only sentences 
%  we generalize Definition~\ref{def:truthVal} as follows:

% \begin{definition}
% \label{def:inOutSolSet}
% Given a formula $\phi$, and a structure $\SStruc$, $x$ is \emph{in (out) of a solution
%   set} of $\phi$ in $\SStruc$ iff there is a quantifier-choice
% $\SQA^{*}$ for $\phi$ such that for all measure-guesses $\SV^{*}$ in $\SStruc$, $x$ is in
% (out) of the solution set of $\phi$ under $\SFInt$.
% \end{definition}

% This is exactly the information we ask for in our specification (figure~\ref{fig:spec}).

\section{Approximate Computation and Approximate Quantifiers}
\label{sec:appr-comp-appr}

The question remains, whether we can solve first-order constraints that contain
approximate instead of classical quantifiers, up to an arbitrarily small error bound. For
this we
%go back to (real) constraint solving by fixing an according structure $\SStruc$, and 
apply our model for approximate computation of Section~\ref{sec:model-appr-comp} to
approximate quantification. The agenda will be, first to show how to propagate \emph{all}
available approximate information, and then to show, how to infer from this the
information needed for our specification in Figure~\ref{fig:spec}.

%\paragraph{Biapproximate Solution Sets}
In Section~\ref{sec:model-appr-comp} we represented the uncertainty about a solution set
by the notion of approximate solution set of a constraint.  In
addition to this, here we also have the \emph{don't know} nondeterminism resulting from
measure guesses. So an \emph{approximate solution set of a constraint $\phi$ under a
  quantifier choice $\SQC$} is a potential approximate solution set that contains all solution sets
of $\phi$ under this quantifier choice $\SQC$ and any measure guess $\SMG$.
% Given a constraint $\phi$, a set of solution sets is an  iff it contains all solution sets of
%   $\phi$ under $\SQC$ and measure guesses $\SMG$.
But in addition to this
nondeterminism, the semantics of our language, as given in Definition~\ref{def:truthVal},
takes into account the \emph{don't care} nondeterminism resulting from quantifier choices. This
means that several different approximate solution sets can be equally valid, depending on
the actual quantifier choice taken. For modeling this situation we introduce a second
level of approximation:

\begin{definition}
  A \emph{potential biapproximate solution set} is a set of potential approximate solution
  sets.  A \emph{biapproximate solution set of $\phi$} is a set of approximate solution
  sets of $\phi$.
\end{definition}

Note that here, when dealing with \emph{don't care} nondeterminism, we approximate the
case of full information, by taking a subset instead of superset of all possible objects.

%Note that if $n=0$ then we speak of (bi)approximate truth-values instead of solution sets.  
% We call the set of all subsets of $\SKAp{\SDen}_{n}$ the set of all
% $n$-dimensional biapproximate solution sets and denote it by $\SBAp{\SDen}_{n}$. 

In general, also for functions one can have these two forms of nondeterminism: On the one
hand, we can have several functions where we \emph{don't know} which is the right one. On
the other hand, we can have several functions where we \emph{don't care} which one is
chosen.  Analogously to solution sets, we model the combination of both by sets of
approximate functions, which we call \emph{biapproximate functions}.

%\paragraph{Spec from Biapproximate Solution sets}
For typesetting reasons, instead of $\SKAp{\SKAp{A}}$ we use the notation $\SBAp{A}$ to
denote biapproximate objects.  Again we can deduce the information that we want to find
for our specification (Figure~\ref{fig:spec}) as follows:

\begin{definition}
\label{def:1}
  A variable assignment $\SVarAss$ is \emph{determined to true} by a potential biapproximate
  solution set $\SBAp{d}$ iff there is a potential approximate solution set $\SKAp{d}\in\SBAp{d}$
  such that $\SVarAss$ is determined to true by $\SKAp{d}$. It is \emph{determined to
    false} by $\SBAp{d}$ iff there is a potential approximate solution set $\SKAp{d}\in\SBAp{d}$
  such $\SVarAss$ is determined to false by $d\in\SKAp{d}$.  It is \emph{determined} by
  $\SBAp{d}$ iff it is either determined to true or determined to false by $\SBAp{d}$.
\end{definition}

Now we again define the error of a potential biapproximate solution set $\SBAp{d}$ as the outer
measure of the set of all variable assignments not determined by $\SBAp{d}$.

%\paragraph{Approximate Projection Operator}
As for classical quantification also approximate quantification results in a function on
potential solution sets:

\begin{definition}
  For a variable $v\in V$, a nonnegative real number $\SQA$, and a possible measure
  $\SV$, the \emph{$(v, \SQA,\SV)$-projection operator  $P_{\SQA,\SV}^{v}$} is a function
 on potential solution sets such that $\SVarAss\in
  P_{\SQA,\SV}^{v}(d)$ iff $\SV(\{ a\in\SStruc \,|\, \SSubs{\SVarAss}{a}{v}\in d\})>\SQA$.
\end{definition}

For a variable $v$ and nonnegative real number $\SQA$, we call the set of all $(v,
\SQA,\SV)$-projection operators \emph{approximate $(v,\SQA)$-projection operator} and
denote it by $P_{\SQA}^{v}$. This is an approximate function. For a fixed $v$ and interval
$\SInt{\SQA}$ we call the set of all $(v, \SQA)$-projection operators, where
$\SQA\in\SInt{\SQA}$, \emph{biapproximate $(v, \SInt{\SQA})$-projection operator}. This is
a biapproximate function.

% %\paragraph{Equivalence: Proj. Op. vs. Logic}
% Assume that we have chosen a certain quantifier choice and that we can fix a certain
% measure guess.  Now it is easy to prove, that the $\SPair{\SQA}$-projection operator
% behaves as desired:

% \begin{lemma}
%   Let $d$ be the solution set of $\phi$ under a quantifier choice $\SQC$ and measure guess
%   $\SMG$. Then $P_{\SQC(t),\SMG{t}}$ is the solution set of $(\exists_{\SInt{\SQA}}^{t})\phi$
%   under $\SQC$ and $\SMG$.
% \end{lemma}

% %\paragraph{Extension to Bipproximate Solution Sets}
% Also a biapproximate function results in a function on biapproximate solution sets:

% %  (because in this paper we mainly deal
% % with the $1$-ary function given by the quantifiers, we restrict ourselves to $1$-ary
% % functions here --- the generalization to $n$-ary functions is trivial).

% \begin{definition}
% \label{def:setExt}
% For a biapproximate function $\SBAp{f}$, for any
% biapproximate solution sets $\SBAp{d}$, 
%   \[ \SExt{\SBAp{f}}(\SBAp{d}):=\{ \SExt{\SKAp{f}}(\SKAp{d}) | \SKAp{f}\in\SBAp{f},
%   \SKAp{d}\in\SBAp{d} \} \] 
% We call $\SExt{\SBAp{f}}$ the \emph{extension of $\SBAp{f}$}.
% \end{definition}

%\paragraph{Equivalence: Extension of Projection Operator vs. Logic}
Now we compute biapproximate solution sets by applying the extension of the functions that
correspond to the logical symbols. 

\begin{lemma}
  Let $\exists_{\SInt{\SQA}}^{t} v\;\phi$ be a constraint, $\SKAp{d}_{\phi}$ an
  approximate solution set of $\phi$ under a quantifier choice $\SQA^{*}$ for
  $\exists_{\SInt{\SQA}}^{t} v\;\phi$, and $P=P_{\SQA^{*}(t)}^{v}$. Then
    $\SExt{P}(\SKAp{d}_{\phi})$ is an approximate solution set of
  $\exists_{\SInt{\SQA}}^{t}\;\phi$ under $\SQA^{*}$.
\end{lemma}

%However, this we can do this propagation on biapproximate solution sets only for free
%constraints:

\begin{theorem}
  Let $\exists_{\SInt{\SQA}}^{t} v\;\phi$ be a constraint such that the tag $t$ does not
  occur in $\phi$, let $\SBAp{d}_{\phi}$ be a biapproximate solution set of $\phi$, and
  let $P$ be the biapproximate $(v, \SInt{q})$-projection operator. Then
  $\SExt{P}(\SBAp{d}_{\phi})$ is a biapproximate solution set of
  $\exists_{\SInt{\SQA}}^{t} v\;\phi$.
\end{theorem}

\begin{proof}
%   Now let $\SKAp{d}$ be an arbitrary but fixed element of $\SExt{\SBAp{P}}(\SBAp{d}_{\phi})$. We have
%   to prove that $\SKAp{d}$ is an approximate solution set of
%   $(\exists_{\SInt{\SQA}}^{t})\phi$.  So we have to prove that there is a quantifier
%   choice $\SQA^{*}$ such that $\SKAp{d}$ is an approximate solution set of
%   $(\exists_{\SInt{\SQA}}^{t})\phi$ under $\SQA^{*}_{\phi}$.
  Let $\SKAp{d}$ be an arbitrary but fixed element of $\SExt{P}(\SBAp{d})$.  We have to
  prove that $\SKAp{d}$ is an approximate solution set of $\exists_{\SInt{\SQA}}^{t}
  v\;\phi$.  By definition of extension we know that there is a
  $\SKAp{d}_{\phi}\in\SBAp{d}_{\phi}$ and a $\SQA\in\SInt{\SQA}$ such that
  $\SKAp{d}=\SExt{P_{q}^{v}}(\SKAp{d}_{\phi})$. By definition of biapproximate
  solution set, $\SKAp{d}_{\phi}$ is an approximate solution set of $\phi$ under a
  quantifier choice $\SQA^{*}_{\phi}$ of $\phi$. Let $\SQA^{*}$ be such that it is equal
  to $\SQA^{*}_{\phi}$ on all tags occurring in $\phi$, and let it assign $\SQA$ to $t$,
  which is possible since $t$ does not occur in $\phi$. Then, by the previous lemma,
  $\SExt{P_{\SQA^{*}(t)}^{v}}(\SKAp{d}_{\phi})=\SKAp{d}$ is an approximate solution set of
  $\exists_{\SInt{\SQA}}^{t} v\;\phi$ under $\SQA^{*}$.  \qed
% By definition of biapproximate solution set
%   there is quantifier choice $\SQA^{*}_{\phi}$, such that $\SKAp{d}_{\phi}$ is an
%   approximate solution set of $\phi$ under $\SQA^{*}_{\phi}$.
  
%   So we have to prove that there is a quantifier choice $\SQA^{*}$ such that
%   $\SExt{P}(\SKAp{d}_{\phi})$ is an approximate solution set of
%   $(\exists_{\SInt{\SQA}}^{t})\phi$.

%   Now choose $\SQA^{*}$ such that it is equal to
%   $\SQA^{*}_{\phi}$ on all tags occuring in $\phi$, and let it assign $\SQA$ to $t$ ---
%   this is possible since $t$ either does not occur in $\phi$, or the according quantifier
%   is deterministic, in which case $\SQA^{*}_{\phi}$ already assigns $\SQA$ to $t$. 
\end{proof}

% \begin{proof}
%   Let $\SKAp{d}$ be an arbitrary but fixed element of $\SExt{\SBAp{P}}(\SBAp{d})$. We have
%   to prove that $\SKAp{d}$ is an approximate solution set of
%   $(\exists_{\SInt{\SQA}}^{t})\phi$.  By definition of extension we know that there is a
%   $\SKAp{d}_{\phi}\in\SBAp{d}$ and an approximate $\SQA$-projection operator $\SKAp{P}$
%   with $\SQA\in\SInt{\SQA}$, such that $\SKAp{d}=\SExt{\SKAp{P}}(\SKAp{d}_{\phi})$. By
%   definition of biapproximate solution set there is quantifier choice $\SQA^{*}_{\phi}$,
%   such that $\SKAp{d}_{\phi}$ is an approximate solution set of $\phi$ under
%   $\SQA^{*}_{\phi}$.  
  
%   So we have to prove that there is a quantifier choice $\SQA^{*}$ such that
%   $\SExt{\SKAp{P}}(\SKAp{d}_{\phi})$ is an approximate solution set of
%   $(\exists_{\SInt{\SQA}}^{t})\phi$. Choose $\SQA^{*}$ such that it is equal to
%   $\SQA^{*}_{\phi}$ on all tags occuring in $\phi$, and let it assign $\SQA$ to $t$ ---
%   this is possible since $t$ either does not occur in $\phi$, or the according quantifier
%   is deterministic, in which case $\SQA^{*}_{\phi}$ already assigns $\SQA$ to $t$. Then
%   $\SKAp{d}=\SExt{\SKAp{P}}(\SKAp{d}_{\phi})$ is an approximate solution set of
%   $(\exists_{\SInt{\SQA}}^{t})\phi$ under $\SQA^{*}$. \qed
% \end{proof}

The condition on the tags is always fulfilled for free constraints. If it does not hold,
the resulting biapproximate solution set might contain elements that are no approximate
solution sets of the constraint. The reason for this is, that the extension does not take
into account tag equality in a similar way as interval arithmetic does not take into
account equality of variables~\cite{Moore:66,Neumaier:90}.

%\paragraph{Projection Operator Allows Approximation?}
% Finally, we adapt the definition of the property needed for a function to be useable for
% computing approximate information up to arbitrary small error.

% \begin{definition}
%   A function $\SBAp{f}:\SBAp{\SDen}_{k}\rightarrow\SBAp{\SDen}_{l}$ is \emph{convergent} iff 
%     for all $\varepsilon\in\mathbb{R}^{+}$
%       there is an $\varepsilon'\in\mathbb{R}^{+}$ such that
%         for all $\SBAp{d}\in\SBAp{\SDen}_{k}$ such that the error of $\SBAp{d}$ is less or equal $\varepsilon'$,
%           the error of $\SBAp{f}(\SBAp{d})$ is less or equal $\varepsilon$.
% \end{definition}

% Again this definition is compatible with the corresponding one in
% Section~\ref{sec:prop-appr-solut}. 


\section{Representing Biapproximate Solution Sets}
\label{sec:repr-appr-solut}

Before studying, whether biapproximate projection is convergent, we first study
biapproximate solution sets in more details.  Observe that different potential biapproximate
solution sets can contain exactly the same information we need to find for fulfilling our
specification in Figure~\ref{fig:spec}.  For example, if we have the biapproximate truth
value $\{ \{ \STrue \} \}$ of a sentence, then we know that the sentence is true.  But, if
we have the biapproximate truth-value $\{ \{ \STrue \}, \{ \STrue, \SFalse \} \}$, then we
have exactly the same information. So there is some interaction between the two forms of
nondeterminism that potential biapproximate solution sets do not explicitely take into account, and
we can divide the potential biapproximate solution sets into equivalence classes such that each
equivalence class element contains the same information.

% Recall that we can compute our specification by treating all logical symbols as functions
% from (bi)approximate solution sets to (bi)approximate solution sets.  

In this section we show, that in many cases it suffices to implement functions on
potential biapproximate solution sets (e.g., projection operators) just on the above equivalence
classes. Since the set of equivalence classes has a much lower cardinality than the full set of
potential biapproximate solution sets, we can then find a representation that is better suited for
computer implementation.  Furthermore we gain a valuable tool for the subsequent proof
that the biapproximate $\SInt{\SQA}$-projection operators are convergent, and find
interesting insight in the interaction between \emph{don't know} and \emph{don't care} nondeterminism.

%\paragraph{Representing Approximate Solution Sets}
Before studying the general case of potential biapproximate solution sets, we start with the easier
case of potential approximate solution sets. The information we want to extract are the elements
determined to true, and the elements determined to false by a potential approximate solution set
$\SKAp{d}$. These are exactly the elements $\bigcap\SKAp{d}$, and all elements not in
$\bigcup\SKAp{d}$. This gives us the equivalence relation $\SKAp{d}_{1}\sim\SKAp{d}_{2}$
iff $(\bigcap\SKAp{d}_{1},\bigcup\SKAp{d}_{1})=(\bigcap\SKAp{d}_{2},\bigcup\SKAp{d}_{2})$.

% (i.e. $r(\SKAp{d}_{1})=r(\SKAp{d}_{1})$ implies
%$r(f(\SKAp{d}_{1}))=r(f(\SKAp{d}_{1}))$).
  
Now let us also define an order $\leq$ on functions on potential approximate solution sets such that
$f_{1}\leq f_{2}$ iff for all $d$, $f_{1}(d)\subseteq f_{2}(d)$. Also here we can form an
equivalence relation on approximate functions by defining $\SKAp{f}_{1}\sim \SKAp{f}_{2}$
iff $(\min\SKAp{f}_{1},\max\SKAp{f}_{1})=(\min\SKAp{f}_{2},\max\SKAp{f}_{2})$. We call a function
$f$ on potential solution sets \emph{monotonic} iff $d_{1}\subseteq d_{2}$ implies
$f(d_{1})\subseteq f(d_{2})$. In a similar way we define an approximate or biapproximate
function to be monotonic iff all its members are monotonic.

For computing with the equivalence classes instead of their members, we need to know
whether all members of equivalence classes behave equally for function application. For
this we pick a $\emph{canonical representative}$ from each equivalence class and prove
that all the other class members behave in the same way as this representative.  We can
order potential approximate solution sets by the subset relation, and so we can also use interval
notation on them: $[\SIntL{d},\SIntR{d}]:= \{ d \:|\: \SIntL{d}\subseteq
d\subseteq\SIntR{d} \}$. Observe that for any potential approximate solution set $\SKAp{d}$, the
interval $r(\SKAp{d}):=[\bigcap\SKAp{d},\bigcup\SKAp{d}]$ is equivalent to $\SKAp{d}$, and
for any approximate function $\SKAp{f}$ the interval
$r(\SKAp{f}):=[\min\SKAp{f},\max\SKAp{f}]$ is equivalent to $\SKAp{f}$. So we take
$r(\SKAp{d})$ and $r(\SKAp{f})$ as the canonical representatives. Now we have the
following congruence property:

% \begin{figure}[htbp]
% \centering ~
% \xymatrix@R=2cm@C=3.5cm{
% \SExt{\SKAp{f}}(\SKAp{d}) \ar[r]^{\mbox{r}} & r(\SExt{\SKAp{f}}(\SKAp{d}))=[\SIntL{f}(\SIntL{d}), \SIntR{f}(\SIntR{d})] \\
% \SKAp{d} \ar[u]_{\SExt{\SKAp{f}}}\ar[r]^{\mbox{r}} & \SInt{d} \ar[u]
% }    
% \caption{Congruence}
% \label{fig:congruence}
% \end{figure}


\begin{lemma}
  For a potential approximate solution set $\SKAp{d}$ with canonical representative $\SInt{d}$ and a
  monotonic approximate function $\SKAp{f}$ with canonical representative $\SInt{f}$,
  $r(\SExt{\SKAp{f}}(\SKAp{d}))=[\SIntL{f}(\SIntL{d}), \SIntR{f}(\SIntR{d})]$.
\end{lemma}

\begin{proof}
By definition, $r(\SExt{\SKAp{f}}(\SKAp{d}))$ is equal to 
\[ [\bigcap\SExt{\SKAp{f}}(\SKAp{d}), \bigcup\SExt{\SKAp{f}}(\SKAp{d})]\]

Now, by inserting the definition of $\SExt{\SKAp{f}}$ and by monotonicity of $\SKAp{f}$
\[ \bigcap\SExt{\SKAp{f}}(\SKAp{d}) = \bigcap \{f(d) \:|\: f\in\SKAp{f}, d\in\SKAp{d} \} = (\min\SKAp{f})(\bigcap\SKAp{d}) = \SIntL{f}(\SIntL{d}) \]
and 
\[ \bigcup\SExt{\SKAp{f}}(\SKAp{d}) = \bigcup\{f(d) \:|\: f\in\SKAp{f}, d\in\SKAp{d} \} = (\max\SKAp{f})(\bigcup\SKAp{d}) = \SIntR{f}(\SIntR{d}). \]
\qed
\end{proof}

% Now it remains to study how to actually do computation on the equivalence classes. We do
% this by picking out a \emph{canonical representative} for each equivalence class and show
% how to do computation in this representative. Let $\SPair{d}$ be the representation of an
% equivalence class, then the interval $\SInt{d}=\{ d | \SIntL{d}\subseteq d\subseteq
% \SIntR{d}\}$ is an element of the corresponding equivalence class, so we take it as its
% canonical representative (this interval is even the biggest possible element of the
% equivalence class, and by taking intervals we do

% \begin{corollary}
%   For a monotonic approximate function $\SInt{f}\subseteq\SDen_{k}\rightarrow\SDen_{l}$,
%   and an approximate solution set $\SInt{d}\in\SKAp{\SDen}_{k}$,
%   $r(\SExt{\SInt{f}}(\SInt{d}))=[\SIntL{f}(\SIntL{d}), \SIntR{f}(\SIntR{d})]$
% \end{corollary}

The $(v, \SQA,\SV)$-projection operators are monotonic. Furthermore the representation of
each approximate $(v, \SQA$)-projection operator is the interval $[P_{\SQA,\SIntL{\SV}}^{v},
P_{\SQA,\SIntR{\SV}}^{v}]$. So we can compute the approximate projection
of a potential approximate solution set by just computing with the interval bounds of the
corresponding representations.

%\paragraph{Generalization to Biapproximate Solution Sets}
Now we study the general case of potential biapproximate solution sets.  In a similar way as
potential approximate solution sets, different potential biapproximate solution sets can yield the same
information. Also here the information we want to extract are the elements determined to
true, and the elements determined to false by a potential biapproximate solution set $\SBAp{d}$ (see
Definition~\ref{def:1}). These are the elements $\bigcup \{ \bigcap\SKAp{d} \,|\,
\SKAp{d}\in\SBAp{d} \}$, and all elements not in $\bigcap \{ \bigcup\SKAp{d} \,|\,
\SKAp{d}\in\SBAp{d} \}$.  Again, this gives us an equivalence relation
$\SBAp{d}_{1}\sim\SBAp{d}_{2}$ iff $(\bigcup \{ \bigcap\SKAp{d} \,|\, \SKAp{d}\in\SBAp{d}_{1}
\},\bigcap \{ \bigcup\SKAp{d} \,|\, \SKAp{d}\in\SBAp{d}_{1} \})= (\bigcup \{ \bigcap\SKAp{d} \,|\,
\SKAp{d}\in\SBAp{d}_{2} \}, \bigcap \{ \bigcup\SKAp{d} \,|\, \SKAp{d}\in\SBAp{d}_{2} \})$. In
a similar way we get an equivalence relation on biapproximate functions by
$\SBAp{f}_{1}\sim\SBAp{f}_{2}$ iff 
$(\max\{ \min\SKAp{f} \,|\, \SKAp{f}\in\SBAp{f}_{1} \},\min\{ \max\SKAp{f} \,|\,
\SKAp{f}\in\SBAp{f}_{1}\}) = (\max\{ \min\SKAp{f} \,|\,\SKAp{f}\in\SBAp{f}_{2} \},\min\{ \max\SKAp{f} \,|\, \SKAp{f}\in\SBAp{f}_{2}\})$.


% $\max\{ \min\SKAp{f} |
%\SKAp{f}\in\SBAp{f}_{1} \} =\max\{ \min\SKAp{f} | \SKAp{f}\in\SBAp{f}_{2}$ and $\min\{
% \max\SKAp{f} | \SKAp{f}\in\SBAp{f}_{1}\}=\min\{ \max\SKAp{f} | \SKAp{f}\in\SBAp{f}_{2}\}$.

Again we pick canonical representatives from the equivalence classes. For any elements
$\SIntL{x}$ and $\SIntR{x}$ in a domain with a partial order $\leq$, let $\SBI{x}:= \{ [
y, y \cup\SIntR{x} ] \,|\, y\in[\SIntL{x}\cap\SIntR{x},\SIntL{x}] \}$. We call such an object
\emph{biinterval} (algebraically speaking the resulting objects form a
bilattice~\cite{Ginsberg:88,Fitting:91}). By forming biintervals we stay within an
equivalence class:

\begin{lemma}
  Let $A$ be a set, let $\SBAp{a}$ an element of the corresponding set $\SBAp{A}$, and let
  $(\SIntL{a}, \SIntR{a})= (\bigcup \{ \bigcap\SKAp{a} | \SKAp{a}\in\SBAp{a} \}, \bigcap \{ \bigcup\SKAp{a} | \SKAp{a}\in\SBAp{a} \})$; then
  $\SBI{a}\sim\SBAp{a}$.
\end{lemma}

\begin{proof}
\begin{multline*}
\bigcup \{ \bigcap\SKAp{a}|\SKAp{a}\in\SBI{a} \} = 
\bigcup \{ \bigcap [ a, a\cup\SIntR{a} ] |a\in[\SIntL{a}\cap\SIntR{a}, \SIntL{a} ] \} =\\
\bigcup \{  a |a\in[\SIntL{a}\cap\SIntR{a}, \SIntL{a} ] \} =
\SIntL{a} = \bigcup \{ \bigcap\SKAp{a} | \SKAp{a}\in\SBAp{a} \}
\end{multline*}

In a similar way $\bigcap \{ \bigcup\SKAp{a}|\SKAp{a}\in\SBI{a} \} = \bigcap \{ \bigcup\SKAp{a} | \SKAp{a}\in\SBAp{a} \}$. \qed
\end{proof}

So again, we denote the canonical representative $\SBIS{\bigcup \{ \bigcap\SKAp{d} |
  \SKAp{d}\in\SBAp{d} \}}{\bigcap \{ \bigcup\SKAp{d} | \SKAp{d}\in\SBAp{d} \}}$ of
$\SBAp{d}$ by $r(\SBAp{d})$, and the canonical representative $\SBIS{\max \{ \min\SKAp{f}
  | \SKAp{f}\in\SBAp{f}\}}{\min \{ \max\SKAp{f} | \SKAp{f}\in\SBAp{f}\} }$ of $\SBAp{f}$
by $r(\SBAp{f})$. Also here we can compute with the representatives because of the
following congruence property:

\begin{theorem}
\label{thm:1}
  For a potential biapproximate solution set $\SBAp{d}$ and a monotonic biapproximate function
  $\SBAp{f}$, 
  $r(\SExt{\SBAp{f}}(\SBAp{d}))=\SBIS{\SIntL{f}(\SIntL{d})}{\SIntR{f}(\SIntR{d})}$, where
  $\SBI{d}=r(\SBAp{d})$, and $\SBI{f}=r(\SBAp{f})$.
\end{theorem}

\begin{proof}
By definition, $r(\SExt{\SBAp{f}}(\SBAp{d}))$ is equal to 
\[\SBIS{
    \bigcup \{ \bigcap \SKAp{d} | \SKAp{d}\in\SExt{\SBAp{f}}(\SBAp{d}) \}
  }{
    \bigcap \{ \bigcup \SKAp{d} | \SKAp{d}\in\SExt{\SBAp{f}}(\SBAp{d}) \}}\]

% Now, by monotonicity 
% \[ \bigcap \{f(d) | f\in\SKAp{f}, d\in\SKAp{d} \} = (\min\SKAp{f})(\bigcap\SKAp{d}) = \SIntL{f}(\SIntL{d}) \]
% and 
% \[ \bigcup \{f(d) | f\in\SKAp{f}, d\in\SKAp{d} \} = (\max\SKAp{f})(\bigcup\SKAp{d}) = \SIntR{f}(\SIntR{d}) \]
% \qed


% By definition of $r$ we have to prove that 
% \[ \bigcup \{ \bigcap\SKAp{d} | \SKAp{d}\in\SExt{\SBI{f}}(\SBI{d}) \} = \SIntL{f}(\SIntL{d}) \]
% and
% \[ \bigcap \{ \bigcup\SKAp{d} | \SKAp{d}\in\SExt{\SBI{f}}(\SBI{d}) \} = \SIntR{f}(\SIntR{d}) \]

We have:
\begin{align*}
\bigcup \{ \bigcap\SKAp{d} | \SKAp{d}\in\SExt{\SBAp{f}}(\SBAp{d}) \} = && \text{def. of Ext}\\
\bigcup \{ \bigcap\SExt{\SKAp{f}}(\SKAp{d}) | \SKAp{f}\in\SBAp{f},\SKAp{d}\in\SBAp{d} \} =&& \text{def. of Ext.}\\
\bigcup \{ \bigcap \{ f(d) | f\in\SKAp{f}, d\in\SKAp{d} \} | \SKAp{f}\in\SBAp{f},\SKAp{d}\in\SBAp{d} \} = && \text{monot.}\\
\bigcup \{ (\min\SKAp{f})(\bigcap\SKAp{d}) | \SKAp{f}\in\SBAp{f},\SKAp{d}\in\SBAp{d} \} = && \text{monot.}\\
(\max \{ \min\SKAp{f} | \SKAp{f}\in\SBAp{f}\})(\bigcup \{ \bigcap\SKAp{d} | \SKAp{d}\in\SBAp{d}\}) = && \text{def. of r}\\
\SIntL{f}(\SIntL{d})
\end{align*}

For the dual case an analogous argument holds. \qed
\end{proof}

For a biapproximate $\SInt{\SQA}$-projection operator $P$, $r(P)$ is the
biinterval $\SBIS{P_{\SIntL{\SQA},\SIntL{\SV}}}{P_{\SIntR{\SQA},\SIntR{\SV}}}$. As a
consequence of the above theorem, for every potential biapproximate solution set $\SBAp{d}$ we can
compute the projection of its equivalence class by just working on the bounds $\SIntL{d}$
and $\SIntR{d}$ of $r(\SBAp{d})$ to get
$\SBIS{P_{\SIntL{\SQA},\SIntL{\SV}}(\SIntL{d})}{P_{\SIntR{\SQA},\SIntR{\SV}}(\SIntR{d})}$.

% \section{Approximate Quantifiers and Approximate Projection}

% We need to study how far the semantics of formulas in this language corresponds to the
% propagation of sets of approximate solution sets. They cannot correspond exactly because
% by propagating sets of approximate solution sets we loose information, by

% \begin{itemize}
% \item not taking into account tag equality between two different quantifiers with
%   the same tag, and by
% \item not using the same quantifier choice when projecting different parts of a solution
%   set.
% \end{itemize}

% So, in general, our propagation method generates more approximate solution sets than
% allowed by the semantics of our language. The first above problem does not occur for free
% formulas. Furthermore we have seen in the last section (lemma~\ref{lem:9}) that for any
% set of approximate solution sets $E$, its pair representation $r(E)$ captures its
% essential information. The approximate quantifiers correspond to the
% $\SPair{\SQA}$-projection operators modulo rounding to pair representation. So the
% propagation method is the same as the language semantics when just looking at this
% essential information of free formulas.

% \begin{theorem}
%   Given a free formula $(\exists_{\SPair{\SQA}} x)\phi$, let $E$ be a set
%   of approximate solution sets of $\phi$, and let $P_{\SPair{\SQA}}$ be the set of
%   $\SPair{\SQA}$-projection operators.  Then there is a set of approximate solution sets
%   $E'$ of $(\exists_{\SPair{\SQA}} x)\phi$ for which
%   $r(E')=\SExt{P_{\SPair{\SQA}}}(r(E))$.
% \end{theorem}

% \begin{proof}
%   The $\SPair{\SQA}$-projection operators form an interval $\SInt{P}$.
%   Let $\SPair{c}=r(E)$. 
%   Then by theorem \ref{thm:1},
%      $\SExt{P_\SPair{\SQA}}(r(E))=(\SIntR{P}(\SIntL{c}),\SIntL{P}(\SIntR{c}))$.
%   So we have to prove that 
%     there is a set of approximate solution sets $E'$ of $(\exists_{\SPair{\SQA}} x)\phi$ for which 
%       $r(E')=(\SIntR{P}(\SIntL{c}),\SIntL{P}(\SIntR{c}))$.
%   We choose $\{ \SIntL{P}(e) | e \in E \} \cup \{ \SIntR{P}(e) | e \in E \}$ for $E'$ and
%   have to prove that
%     $r(E')=(\SIntR{P}(\SIntL{c}),\SIntL{P}(\SIntR{c}))$.
%   So we have to prove that
%     $\bigcup \{ \bigcap e | e\in E' \}=\SIntR{P}(\SIntL{c})$
%   and 
%     $\bigcap \{ \bigcup e | e\in E' \}=\SIntL{P}(\SIntR{c})$.

%   The first equation can be proved as follows:
% \begin{multline*}
%   \bigcup \{ \bigcap e | e\in E' \}= 
%   \bigcup \{ \bigcap e | e\in \{ \SIntL{P}(e) | e \in E \} \cup \{ \SIntR{P}(e) | e \in E \} \}= \\
%   \bigcup \{ \bigcap e | e\in \{ \SIntR{P}(e) | e \in E \} \}= 
%   \bigcup \{ \bigcap \SIntR{P}(e) | e \in E \} = \\
%   \SIntR{P}(\bigcup \{ \bigcap e | e\in E \}) = 
%   \SIntR{P}(\SIntL{c})
% \end{multline*}
% The second equation can be proved analogously. \qed
% \end{proof}

\section{Biapproximate Projection is Convergent}
\label{sec:biappr-proj-conv}

%%\paragraph{Biapproximate Projection and Error on Pairs}

% \begin{lemma}
%   Let $\SInt{c}$ be the representation of a biapproximate solution set $\SBAp{d}$, and let
%   $P$ be the biapproximate $\SInt{\SQA}$-projection operator. Then
%   $\SExt{P}(\SBAp{d})=\SInt{p}$, where $\SIntL{p}$ is the set of all $(x_{1},\dots,x_{n})$
%   for which $\SIntR{\SV}(\{ y | (x_{1},\dots,x_{n},y)\in\SIntL{c}\})>\SIntR{\SQA}$, and
%   $\SIntL{p}$ is the set of all $(x_{1},\dots,x_{n})$ for which $\SIntL{\SV}(\{ y |
%   (x_{1},\dots,x_{n},y)\in\SIntR{c}\})>\SIntL{\SQA}$.
% \end{lemma}

% \begin{lemma}
%   Let $\SInt{c}$ be the representation of a biapproximate solution set $\SBAp{d}$, then
%   the error of $\SBAp{d}$ is the the outer measure of all $x$ for which
%   $x\not\in\SIntL{c}$, and $x\in\SIntR{c}$.
% \end{lemma}

%\paragraph{Pairs Contract}

Now we are ready to prove that for approximate quantifiers we can compute approximate
solution sets of constraints up to arbitrarily small error bounds. For this we call a
potential biapproximate solution set that contains only measurable solution sets \emph{measurable}.

\begin{definition}
  Let $\SBAp{d}$ be a potential biapproximate solution set. For any variable assignment $\SVarAss$
  the \emph{$v$-error of $\SBAp{d}$ over $\SVarAss$} is the outer measure of all
  $a\in\SStruc$ for which $\SSubs{\SVarAss}{a}{v}$ is not determined by $\SBAp{d}$.
\end{definition}

We first prove that for single points in the free variable space
we can attain an arbitrarily small error.

%, because for
%arbitrary small input error always either the minimal or the maximal projection operator
%determines the result.

\begin{lemma}
\label{lem:4}
For every measurable potential biapproximate solution set $\SBAp{d}$, for the
biapproximate $(v, \SInt{q})$-projection operator P with $\SIntL{\SQA}<\SIntR{\SQA}$, for
almost all variable assignments $\SVarAss$ such that $\SVarAss$ is not determined by
$r(\SExt{P}(\SBAp{d}))$, the $v$-error of $\SBAp{d}$ over $\SVarAss$ is greater than
$\SIntR{\SQA}-\SIntL{\SQA}$.
\end{lemma}

\begin{proof}
  Observe that a variable assignment $\SVarAss$ is not determined by a potential biapproximate
  solution set with representation $\SBI{d}$ iff $\SVarAss\not\in\SIntL{d}$ and
  $\SVarAss\in\SIntR{d}$.  Let $r(d)=\SBI{d}$ and let $\SVarAss$ be such that it is not
  determined by $r(\SExt{P}(\SBI{d}))$, which is
  $\SBIS{P_{\SIntL{\SQA},\SIntL{\SV}}^{v}(\SIntL{d})}{P_{\SIntR{\SQA},\SIntR{\SV}}^{v}(\SIntL{d})}$
  by Theorem~\ref{thm:1}.  So, by definition of projection operator, $\SIntL{\SV}(\{ a \,|\,
  \SSubs{\SVarAss}{a}{v}\in\SIntL{d} \})\leq\SIntL{\SQA}$ and $\SIntR{\SV}(\{ a \,|\,
  \SSubs{\SVarAss}{a}{v}\in\SIntR{d} \})>\SIntR{\SQA}$. Since $\SIntL{d}$ and $\SIntR{d}$
  are measurable, by Fubini's theorem, the sets $\{ a \,|\,
  \SSubs{\SVarAss}{a}{v}\in\SIntL{d} \}$ and $\{ a \,|\,
  \SSubs{\SVarAss}{a}{v}\in\SIntR{d} \}$ are  measurable for almost all $\SVarAss$.
% So the volume of is less or equal $\SIntL{\SQA}$,
%   and the volume of the $a$ that are not determined to false by $\SBI{d}$ is greater than
%   $\SIntR{\SQA}$. 
  The $\SVarAss$ that are not determined by $\SBI{d}$ are represented by the set $\{ a\:|\:
  \SSubs{\SVarAss}{a}{v}\not\in\SIntL{d}\:\wedge\:
  \SSubs{\SVarAss}{a}{v}\in\SIntR{d}\}$. Clearly the volume of this set 
  is greater than $\SIntR{\SQA}-\SIntL{\SQA}$.  \qed
\end{proof}


Since we have shown in the last section that for computing our specification
(Figure~\ref{fig:spec}), we can apply the canonical representative of projection operators
instead of the projection operators themselves, we now prove:

\begin{theorem}
  For $\SIntL{\SQA}<\SIntR{\SQA}$, and the biapproximate $(v, \SInt{\SQA})$-projection operator
  $P$, $r \circ \SExt{P}$ restricted to measurable potential biapproximate solution sets is convergent.
\end{theorem}

\begin{proof}
  We have to prove that
    for all $\varepsilon\in\mathbb{R}^{+}$,
      there is a $\delta\in\mathbb{R}^{+}$ such that
        for every measurable potential biapproximate solution set $\SBAp{d}$ such that the error of $\SBAp{d}$ is less than $\delta$,
          the error of $r(\SExt{P}(\SBAp{d}))$ is less than $\varepsilon$.
          
  Choose $(\SIntR{\SQA}-\SIntL{\SQA})\varepsilon$ for $\delta$, and let
  $\SBAp{d}$ be an arbitrary but fixed measurable potential biapproximate solution set. 
%
  We derive a contradiction from the assumption that the error of $\SBAp{d}$ 
  is less than $(\SIntR{\SQA}-\SIntL{\SQA})\varepsilon$, but the error of
  $r(\SExt{P}(\SBAp{d}))$ is greater or equal $\varepsilon$.

  By Lemma~\ref{lem:4}, for almost every $\SVarAss$ that is not determined by
  $r(\SExt{P}(\SBAp{d}))$ the $v$-error of $\SBAp{d}$ over $\SVarAss$ is greater 
  than $\SIntR{\SQA}-\SIntL{\SQA}$. The measure of these  $\SVarAss$ is greater or equal
   $\varepsilon$. So, by Fubini's theorem, the error of $\SBAp{d}$ is greater than
   $(\SIntR{\SQA}-\SIntL{\SQA})\varepsilon$, which is contradiction to our assumption. \qed

% \begin{figure}[htbp]
% \begin{center}
%     \input{proof4.pstex_t}
%     \caption{Error Propagation for Approximate Projection}
%     \label{fig:apprProjContr}
% \end{center}
% \end{figure}

% Now we proceed according to figure~\ref{fig:apprProjContr}.  Let $U$ be the set of the
% $(x_{1},\dots,x_{n})$, for which the volume of the $y$, for which the error of $\SBAp{d}$
% over $(x_{1},\dots,x_{n}$, is greater than $\SIntR{\SQA}-\SIntL{\SQA}$.  Let $U'$ be the
% set of $(x_{1},\dots,x_{n}, y)$, for which $(x_{1},\dots,x_{n})\in U$, and
% $(x_{1},\dots,x_{n})$ is not determined by $\SBAp{d}$.  By Fubini's theorem, the volume of
% $U'$ is greater than $(\SIntR{\SQA}-\SIntR{\SQA})\SV(U)$. Since $U'$ is a subset of all
% the $(x_{1},\dots,x_{n})$ that are not determined by $\SBAp{d}$,
% $(\SIntR{\SQA}-\SIntR{\SQA})\SV(U)<(\SIntR{\SQA}-\SIntL{\SQA})\varepsilon$. Thus the
% volume of $U$ is smaller than $\varepsilon$. Since, by lemma~\ref{lem:4}, all elements not
% in $U$ are determined by $\SBAp{d}$, the error of $\SBAp{d}$ is also smaller than
% $\varepsilon$.  \qed
\end{proof}

Note that, if unmeasurable sets occur, then we still can ensure that the projection
operator is convergent, by making the interval $\SInt{\SQA}$ big enough. In general, we
can make computation faster by increasing the size of the interval $\SInt{\SQA}$, that is,
by decreasing the required precision.

% On the
% other hand, one could extend the language to allow biinterval annotations. In this case
% $\SIntL{\SQA}$ could be bigger than $\SIntR{\SQA}$, which means that we deliberately do
% not derive any information for solution sets whose size is between $\SIntR{\SQA}$ and
% $\SIntL{\SQA}$.

In a similar way as the projection operators for quantifiers, also for the other logical
symbols ($\vee$, $\wedge$, $\neg$) there are corresponding functions on potential solution
sets~\cite{Ratschan:00}, and for free constraints we can use their extension to propagate
the according potential biapproximate solution sets.  The functions corresponding to
conjunction and disjunction are monotonic, and for the function $N$ corresponding to
negation, $d_{1}\subseteq d_{2}$ implies $N(d_{1}\supseteq d_{2})$, which entails a
similar property as Theorem~\ref{thm:1}. So we can use biinterval representation also
here.  

As an example take the constraint $x^2+y^2\leq 1$ and the biinterval
$\SBIS{\emptyset}{S_1}$, where the potential solution set $S_1$ is the set of all variable
assignments that assign elements of $[-1, 1]$ to both $x$ and $y$. This determines all
elements outside of the rectangle $[-1, 1]\times [-1, 1]$ to false and leaves the other
elements undetermined.  Furthermore, take the constraint $x\geq 0$ and the biinterval
$\SBIS{\emptyset}{S_2}$, where $S_2$ is the set of all variable assignments. This leaves all
variable assignments undetermined. The solution set of a conjunction is the intersection
of the solution sets of the according sub-constraints, and intersection is monotonic. So by
Theorem~\ref{thm:1} we can  take the intersection of the corresponding biinterval elements,
which is $\emptyset\cap\emptyset$ and $S_1\cap S_2$, and get the biinterval
$\SBIS{\emptyset}{S_1}$ as a biapproximate solution set for $x^2+y^2\leq 1\wedge x\geq 0$.

One can easily show that the functions corresponding to $\vee$,
$\wedge$, and $\neg$ are convergent.  So we can compute approximate solution sets of free
constraints from approximate solution sets of their atomic sub-constraints, as described
in Section~\ref{sec:prop-appr-solut}.  Furthermore---as long as no unmeasurable solution
sets occur and provided that for all approximate quantifiers the left bound $\SIntL{\SQA}$
of the annotation is strictly smaller than the right bound $\SIntR{\SQA}$---we can
attain arbitrarily small, user-defined, error.

\section{Related Work}
\label{sec:related-work}

Languages for modeling nondeterminism in various other forms have been introduced within
the frame of abstract data types---see for
example~\cite{Walicki:97,Walicki:95,Hesselink:88,Hussmann:93}.  There one uses
nondeterministic specifications to either model nondeterminism occurring in reality, or to
abstract away unnecessary details of the behavior of a real or desired system; these
details might be specified later. Also in analysis nondeterminism has been modeled in
order to deal with unknown/uncertain knowledge, and a large amount of classical
analysis has been extended to this case~\cite{Aubin:90,Aubin:91}.

In contrast to the above cases, in our work the deterministic (exact) specification is
already given, and we introduce nondeterminism only later, in order to be able to do
approximate computation for a relaxed specification.  Furthermore we deal with two forms
of nondeterminism at the same time whereas the above approaches are always confined to one
form of nondeterminism.

The idea to allow several equally valid outputs (i.e., \emph{don't care} nondeterminism) to make
certain problems computable is frequently used when doing exact numerical computation on the
reals via potentially infinite representations~\cite{Brouwer:20,Wiedmer:80,Weihrauch:00}. 

% Brower, who showed that the computable real numbers need a
% redundant representation in order to arrive at terminating computation. 

% Similar ideas are
% nowadays frequently used for being able to do approximate computation for other inherently
% discontinuous problems (e.g., GCD-computation~\cite{Schoenhage:85}). In our work, we have
% the additional difficulties, that we have two different kinds of nondeterminism and both
% of them need to be recursively propagated.

Modifications of the first-order language that allow reasoning about the size of sets have
been studied coming from logic~\cite{Keisler:85}, or knowledge
representation~\cite{Bacchus:90,Bacchus:90a}, and they are a main topic in the area of generalized
quantifiers~\cite{Mostowski:57,Vaeaenaenen:97}. However, these languages do not allow any
nondeterministic choice of the size specification and they circumvent the problem of how
to deal with unmeasurable sets by allowing only expressions whose solution sets are
measurable.

\section{Conclusion}
\label{sec:conclusion}

% We have shown how it is possible to compute approximate solution sets of the atomic
% sub-constraints of a first-order constraint up to arbitrary small error bounds, then this
% information suffices for computing

% how to compute approximate solution sets of first-order constraints up to a
% user-specified error bound, . 

For constraints containing classical quantifiers, information about approximate solution
sets of the atomic sub-constraints of a first-order constraint does not suffice to compute
abitrarily precise approximate solution sets of the whole constraints. We have provided a
remedy for this problem by replacing the classical quantifiers in the first-order
predicate language by approximate quantifiers.

In addition to enabling approximation algorithms, this gives us both expressive power in
reasoning and the possibility of tunable algorithms (algorithms where the user can decide
about the tradeoff between speed and precision). We have implemented such an algorithm---a
detailed description and analysis of this implementation will be published elsewhere.

The question remains, how big we should choose the intervals of the quantifier annotation.
Too small intervals can hamper the efficiency of constraint solving, while too big
intervals can disturb the information one is looking for. 
%Regularization
%theory~\cite{Engl:93} provides various tools for this choice; thus we will try to apply it
%here.

%Furthermore our representation of biapproximate objects amounts to some form of
%rounding~\cite{Albrecht:80,Kulisch:80,Kulisch:81}). 
%Future work will clarify the details.

%discuss problems with equalities


Most of this research was done as a part of the author's Ph.D. work. The author thanks his
Ph.D. advisor, Hoon Hong, for all the guidance.





\small


\bibliographystyle{abbrv}


\bibliography{sratscha,sratscha_own}



\end{document}




setup.tex
\usepackage{ifthen}

%----------------------------------
% Theorem-like structures
%----------------------------------
\ifthenelse{\isundefined{\definition}}{\newtheorem{definition}{Definition}}{}
\newtheorem{notations}{Notations}
\ifthenelse{\isundefined{\theorem}}{\newtheorem{theorem}{Theorem}}{}
\ifthenelse{\isundefined{\lemma}}{\newtheorem{lemma}{Lemma}}{}
\ifthenelse{\isundefined{\corollary}}{\newtheorem{corollary}{Corollary}}{}
%\newtheorem{proposition}{Proposition}
%\newtheorem{conjecture}{Conjecture}
%\newtheorem{alg}{Algorithm}
%\newtheorem{exam}{Example}
\ifthenelse{\isundefined{\example}}{\newtheorem{example}{Example}}{}
\ifthenelse{\isundefined{\property}}{\newtheorem{property}{Property}}{}
%\newtheorem{remark}{Remark}
%\newenvironment{example}{\begin{exam}\rm}{\end{exam}}
\ifthenelse{\isundefined{\proof}}{\newenvironment{proof}{\noindent{\bf Proof.}\hspace{0.05in}}{\par\mbox{}\par}}{}


\newcommand{\vs}{\vspace{0.3cm}}
\newcommand{\hs}{\hspace{0.3cm}}
\ifthenelse{\isundefined{\qed}}{\newcommand{\qed}{\mbox{$\blacksquare$}}}{}

%----------------------------------
% Hyphenation
%----------------------------------
\hyphenation{}


%----------------------------------
%   Picture unit length
%----------------------------------
\setlength{\unitlength}{6pt}


%----------------------------------
%  Special symbols
%----------------------------------
\newcommand{\BB}{\mathbb{B}}
\newcommand{\FF}{\mathbb{F}}
\newcommand{\HH}{\mbox{$\mathbb{ H}$}}
\newcommand{\NN}{\mbox{$\mathbb{ N}$}}
\newcommand{\ZZ}{\mbox{$\mathbb{ Z}$}}
\newcommand{\QQ}{\mbox{$\mathbb{ Q}$}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\CC}{\mbox{$\mathbb{ C}$}}


%-----------------------------------
%  Lists
%-----------------------------------
\newenvironment{glists}[4]{
                 \begin{list}{}{
                     \setlength{\labelwidth}{#2}
                     \setlength{\labelsep}{#3}
                     \setlength{\leftmargin}{#1}
                     \addtolength{\leftmargin}{\labelwidth}
                     \addtolength{\leftmargin}{\labelsep}
                     \setlength{\parsep}{#4}
                     \setlength{\topsep}{\parsep}
                     \setlength{\itemsep}{\parsep}
                     \setlength{\listparindent}{0in}
                     }
                 }{
                 \end{list}
                 }
\newenvironment{lists}[1]{
                 \begin{list}{}{
                     \setlength{\listparindent}{0in}
                     \settowidth{\labelwidth}{#1}
                     \setlength{\leftmargin}{\labelwidth}
                     \addtolength{\leftmargin}{\labelsep}
                     }
                 }{
                 \end{list}
                 }
\newenvironment{dlists}[1]{
                 \begin{list}{}{
                     \setlength{\listparindent}{0in}
                     \settowidth{\labelwidth}{#1}
                     \setlength{\leftmargin}{\labelwidth}
                     \addtolength{\leftmargin}{\labelsep}
                     \setlength{\parsep}{0in}
                     \setlength{\topsep}{0in}
                     \setlength{\itemsep}{0in}
                     }
                 }{
                 \end{list}
                 }

%\newenvironment{problem}[4]{
%                 \begin{figure}[h]
%                   \begin{center}
%                     \fbox{
%                     \parbox{\textwidth}{
%                                    \small
%                                    \begin{lists}{Given:XX}
%                                           \item[\sc Given: \hfill] #3
%                                           \item[\sc Find: \hfill] #4
%                                    \end{lists}
%                                    }
%                           }
%                           \caption{#1}
%                           \label{fig:#2}
%                           }{
%                         \end{center}
%                       \end{figure}
%                       }

\newenvironment{given-find}[2]{
                               \vs 
                               \noindent \hrule
%                               \small
                               \begin{lists}{Given:XX}
                               \item[\sc Given: \hfill] #1                                 
                               \item[\sc Find: \hfill] #2                               
                               \vs 
                               \noindent \hrule 
                               }{
                               \end{lists}
%                               \vs
                               }

\newcommand{\iteml}[1]{\item[#1 \hfill]}
\newcommand{\itemr}[1]{\item[\hfill #1]}
\newcommand{\itemc}[1]{\item[\hfill #1 \hfill]}
\newcommand{\bitem}[1]{\item[$\bullet$ #1 \hfill]}
\newcommand{\ditem}[1]{\item[$\diamond$ #1 \hfill]}

\newcommand{\defbycase}[5]{\[ {#1} = \left\{ \begin{array}{ll}
                                           {#2} & \mbox{if $#3$ }\\[2ex]
                                           {#4} & \mbox{if $#5$ }
                                          \end{array} \right. \]  }

\newcommand{\defbyonecase}[4]{ {#1} = \left\{ \begin{array}{ll}
                                           {#2} & \mbox{if $#3$ }\\[2ex]
                                           {#4} & \mbox{otherwise}
                                          \end{array} \right.  }

%--------------------------------------
%  Algorithm
%--------------------------------------
%\newenvironment{algorithm}[1]{\noindent \hrule\vs \begin{center} #1 \end{center}
%               }{
%               \vs \noindent \hrule
%               }
%\newenvironment{slidealgorithm}[1]{\begin{center} #1 \end{center}
%               }{
%               }
%\newcommand{\algol}[1]{\begin{center} #1 \end{center}}
%\newenvironment{parms}{\begin{psteps}}{\end{psteps}}
%\newcommand{\inputs}{\iteml{\it Input:}}
%\newcommand{\outputs}{\iteml{\it Output:}}
%\newcommand{\locals}{\iteml{\it Local:}}
%\newcommand{\globals}{\iteml{\it Global:}}
%\newcommand{\remarks}{\iteml{\it Remark:}}
%\newcommand{\spec}{\iteml{\it Spec:}}
%\newcommand{\step}[1]{\item[(#1)]}
%\newenvironment{scode}{
%               \begin{flushleft}
%                     \setlength{\parsep}{0in}
%                     \setlength{\topsep}{0in}
%                     \setlength{\partopsep}{0.3ex}
%                     \setlength{\itemsep}{0.3ex}
%                     \setlength{\listparindent}{0in}
%                     \settowidth{\labelwidth}{(9)}
%                     \setlength{\leftmargin}{\labelwidth}
%                     \addtolength{\leftmargin}{\labelsep}
%               }{\end{flushleft}}
%\newenvironment{steps}{
%               \begin{list}{}{
%                     \setlength{\parsep}{0in}
%                     \setlength{\topsep}{0in}
%                     \setlength{\partopsep}{0.3ex}
%                     \setlength{\itemsep}{0.3ex}
%                     \setlength{\listparindent}{0in}
%                     \settowidth{\labelwidth}{(9)}
%                     \setlength{\leftmargin}{\labelwidth}
%                     \addtolength{\leftmargin}{\labelsep}
%                     }
%               }{
%               \end{list}
%               }
%\newenvironment{psteps}{
%               \begin{list}{}{
%                     \setlength{\parsep}{0in}
%                     \setlength{\topsep}{0in}
%                     \setlength{\partopsep}{1.5ex}
%                     \setlength{\itemsep}{1.5ex}
%                     \setlength{\listparindent}{0in}
%                     \settowidth{\labelwidth}{\em Globals:: }
%                     \setlength{\leftmargin}{\labelwidth}
%                     \addtolength{\leftmargin}{\labelsep}
%                     }
%               }{
%               \end{list}
%               }
%\newenvironment{ssteps}{
%               \begin{list}{}{
%                     \setlength{\parsep}{0in}
%                     \setlength{\topsep}{0in}
%                     \setlength{\partopsep}{1.5ex}
%                     \setlength{\itemsep}{0in}
%                     \setlength{\listparindent}{0in}
%                     \settowidth{\labelwidth}{(9999)}
%                     \setlength{\leftmargin}{\labelwidth}
%                     \addtolength{\leftmargin}{\labelsep}
%                     }
%               }{
%               \end{list}
%               }




apprquantgen.bbl
\begin{thebibliography}{10}

\bibitem{Aubin:91}
J.-P. Aubin.
\newblock {\em Viability Theory}.
\newblock Birkh\"auser, 1991.

\bibitem{Aubin:90}
J.-P. Aubin and H.~Frankowska.
\newblock {\em Set-valued Analysis}.
\newblock Birkh\"auser, Boston, 1990.

\bibitem{Bacchus:90}
F.~Bacchus.
\newblock Lp, a logic for representing and reasoning with statistical
  knowledge.
\newblock {\em Computational Intelligence}, 6:209--231, 1990.

\bibitem{Bacchus:90a}
F.~Bacchus.
\newblock {\em Representing and Reasoning with Probabilistic Knowledge}.
\newblock MIT Press, 1990.

\bibitem{Benhamou:00a}
F.~Benhamou, F.~Goualard, {\'E}.~Langu{\'e}nou, and M.~Christie.
\newblock Universally quantified constraint solving: an application to camera
  control.
\newblock Technical Report 00.5, Institut de Recherche en Informatique de
  Nantes, 2000.
\newblock Submitted for Publication.

\bibitem{Bishop:67}
E.~Bishop.
\newblock {\em Foundations of Constructive Analysis}.
\newblock McGraw Hill, 1967.

\bibitem{Bishop:85}
E.~Bishop and D.~Bridges.
\newblock {\em Constructive Analysis}.
\newblock Springer, 1985.

\bibitem{Bouchon-Meunier:96}
B.~Bouchon-Meunier and V.~Kreinovich.
\newblock From interval computations to modal mathematics: Applications and
  computational complexity.
\newblock {\em ACM SIGSAM Bulletin}, 32(2):7--11, 1998.

\bibitem{Brouwer:20}
L.~Brouwer.
\newblock {Besitzt jede reelle Zahl eine Dezimalbruchentwicklung?}
\newblock {\em Mathematische Annalen}, 83:201--210, 1920.

\bibitem{Caviness:98}
B.~F. Caviness and J.~R. Johnson, editors.
\newblock {\em Quantifier Elimination and Cylindrical Algebraic Decomposition}.
\newblock Springer, Wien, 1998.

\bibitem{Davenport:88}
J.~H. Davenport and J.~Heintz.
\newblock Real quantifier elimination is doubly exponential.
\newblock {\em Journal of Symbolic Computation}, 5:29--35, 1988.

\bibitem{Dolzmann:97}
A.~Dolzmann, T.~Sturm, and V.~Weispfenning.
\newblock Real quantifier elimination in practice.
\newblock In B.~H. Matzat, G.-M. Greuel, and G.~Hiss, editors, {\em Algorithmic
  Algebra and Number Theory}, pages 221--248. Springer, 1998.

\bibitem{Dorato:95}
P.~Dorato, W.~Yang, and C.~Abdallah.
\newblock Robust multi-objective feedback design by quantifier elimination.
\newblock {\em Journal of Symbolic Computation}, 24:153--159, 1997.

\bibitem{Fischer:74}
M.~J. Fischer and M.~O. Rabin.
\newblock Super-exponential complexity of presburger arithmetic.
\newblock {\em SIAM-AMS Proceedings}, 7:27--41, 1974.
\newblock Also in~\cite{Caviness:98}.

\bibitem{Fitting:91}
M.~Fitting.
\newblock Bilattices and the semantics of logic programming.
\newblock {\em Journal of Logic Programming}, 11(2):91--116, 1991.

\bibitem{Gardenes:01}
E.~Garde{\~n}es, M.~{\'A}. Sainz, L.~Jorba, R.~Calm, R.~Estela, H.~Mielgo, and
  A.~Trepat.
\newblock Modal intervals.
\newblock {\em Reliable Computing}, 7(2):77--111, 2001.

\bibitem{Ginsberg:88}
M.~L. Ginsberg.
\newblock Multivalued logics: A uniform approach to reasoning in artificial
  intelligence.
\newblock {\em Computational Intelligence}, 4:265--316, 1988.

\bibitem{GonzalezVega:96}
L.~Gonzalez-Vega.
\newblock A combinatorial algorithm solving some quantifier elimination
  problems.
\newblock In Caviness and Johnson \cite{Caviness:98}.

\bibitem{Halmos:50}
P.~Halmos.
\newblock {\em Measure Theory}.
\newblock Van Nostrand, 1950.

\bibitem{Hehner:84}
E.~Hehner.
\newblock Predicative programming.
\newblock {\em Communications of the ACM}, 27:134--151, Feb. 1984.

\bibitem{Hesselink:88}
W.~H. Hesselink.
\newblock A mathematical approach to nondeterminism in data types.
\newblock {\em {ACM} Transactions on Programming Languages and Systems},
  10(1):87--117, 1988.

\bibitem{Hoare:98}
C.~Hoare and H.~Jifeng.
\newblock {\em Unifying Theories of Programming}.
\newblock Series in Computer Science. Prentice Hall, 1998.

\bibitem{Hong:93a}
H.~Hong.
\newblock Quantifier elimination for formulas constrained by quadratic
  equations via slope resultants.
\newblock {\em The Computer Journal}, 36(5):440--449, 1993.
\newblock Special issue on computational quantifier elimination.

\bibitem{Hong:95c}
H.~Hong.
\newblock Symbolic-numeric methods for quantified constraint solving.
\newblock In {\em International Symposium on Scientific Computing, Computer
  Arithmetic and Validated Numerics SCAN-95}, 1995.
\newblock Invited Talk.

\bibitem{Hong:97}
H.~Hong, R.~Liska, and S.~Steinberg.
\newblock Testing stability by quantifier elimination.
\newblock {\em Journal of Symbolic Computation}, 24(2):161--187, 1997.

\bibitem{Hussmann:93}
H.~Hussmann.
\newblock {\em Nondeterminism in Algebraic Specifications and Algebraic
  Programs}.
\newblock Birkh\"{a}user, 1993.

\bibitem{Jaulin:01b}
L.~Jaulin, M.~Kieffer, O.~Didrit, and E.~Walter.
\newblock {\em Applied Interval Analysis, with Examples in Parameter and State
  Estimation, Robust Control and Robotics}.
\newblock Springer, Berlin, 2001.

\bibitem{Jirstrand:96}
M.~Jirstrand.
\newblock {\em Algebraic Methods for Inequality Constraints in Control}.
\newblock PhD thesis, Link{\"o}ping University, Department of Electrical
  Engineering, Division of Automatic Control, 1998.
\newblock No. 527.

\bibitem{Keisler:85}
H.~J. Keisler.
\newblock Probability quantifiers.
\newblock In J.~Barwise and S.~Feferman, editors, {\em Model Theoretic Logics},
  chapter XIV. Springer Verlag, New York, 1985.

\bibitem{Moore:66}
R.~E. Moore.
\newblock {\em Interval Analysis}.
\newblock Prentice Hall, Englewood Cliffs, NJ, 1966.

\bibitem{Mostowski:57}
A.~Mostowski.
\newblock On a generalization of quantifiers.
\newblock {\em Fundamenta Mathematicae}, 44:12--36, 1957.

\bibitem{Neumaier:90}
A.~Neumaier.
\newblock {\em Interval Methods for Systems of Equations}.
\newblock Cambridge Univ. Press, Cambridge, 1990.

\bibitem{Pour-El:89}
M.~B. Pour-El and J.~I. Richards.
\newblock {\em Computability in Analysis and Physics}.
\newblock Springer-Verlag, 1989.

\bibitem{Ratschan:00}
S.~Ratschan.
\newblock Uncertainty propagation in heterogeneous algebras for approximate
  quantified constraint solving.
\newblock {\em Journal of Universal Computer Science}, 6(9), 2000.

\bibitem{Ratschan:01e}
S.~Ratschan.
\newblock Applications of quantified constraint solving over the reals---
  bibliography.
\newblock \url{http://www.mpi-sb.mpg.de/~ratschan/appqcs.html}, 2001.

\bibitem{Rescher:69}
N.~Rescher.
\newblock {\em Many-valued Logic}.
\newblock McGraw-Hill, New York, 1969.

\bibitem{Richardson:68}
D.~Richardson.
\newblock Some undecidable problems involving elementary functions of a real
  variable.
\newblock {\em Journal of Symbolic Logic}, 33:514--520, 1968.

\bibitem{Shary:96}
S.~P. Shary.
\newblock Algebraic approach to the interval linear static identification,
  tolerance, and control problems, or one more application of {Kaucher}
  arithmetic.
\newblock {\em Reliable Computing}, 2(1):3--33, 1996.

\bibitem{Tarski:51}
A.~Tarski.
\newblock {\em A Decision Method for Elementary Algebra and Geometry}.
\newblock Univ. of California Press, Berkeley, 1951.
\newblock Also in~\cite{Caviness:98}.

\bibitem{Urquhart:86}
A.~Urquhart.
\newblock Many-valued logic.
\newblock In D.~Gabbay and F.~Guenther, editors, {\em Handbook of Philosophical
  Logic, Vol. III: Alternatives in Classical Logic}, chapter III.2, pages
  71--116. D. Reidel Publishing Company, 1986.

\bibitem{Vaeaenaenen:97}
J.~V{\"a\"an\"a}nen.
\newblock Generalized quantifiers.
\newblock {\em Bulletin of the European Association for Theoretical Computer
  Science}, June 1997.

\bibitem{Walicki:95}
M.~Walicki and S.~Meldal.
\newblock A complete calculus for the multialgebraic and functional semantics
  of nondeterminism.
\newblock {\em {ACM} Transactions on Programming Languages and Systems},
  17(2):366--393, 1995.

\bibitem{Walicki:97}
M.~Walicki and S.~Meldal.
\newblock Algebraic approaches to nondeterminism: An overview.
\newblock {\em {ACM} Computing Surveys}, 29(1):30--81, 1997.

\bibitem{Weihrauch:00}
K.~Weihrauch.
\newblock {\em Introduction to Computable Analysis}.
\newblock Texts in Theoretical Computer Science. Springer, Heidelberg, 2000.

\bibitem{Weispfenning:88}
V.~Weispfenning.
\newblock The complexity of linear problems in fields.
\newblock {\em Journal of Symbolic Computation}, 5(1--2):3--27, 1988.

\bibitem{Weispfenning:94}
V.~Weispfenning.
\newblock Quantifier elimination for real algebra --- the cubic case.
\newblock In {\em Proc. ISSAC'94}, pages 258--263, Oxford, 1994. ACM Press.

\bibitem{Wiedmer:80}
E.~Wiedmer.
\newblock Computing with infinite objects.
\newblock {\em Theoretical Computer Science}, 10:133--155, 1980.

\end{thebibliography}
