
\documentstyle[jair, twoside, 11pt, epic, eepic]{article}


\newcommand{\ifff}{\mbox{$\Leftrightarrow$}}
\newcommand{\implies}{\mbox{$\Rightarrow$}}
\newcommand{\goesto}{\mbox{$\rightarrow$}}
\newcommand{\fa}{\mbox{$\forall$}}
\newcommand{\te}{\mbox{$\exists$}}
\newcommand{\ts}{\mbox{$\vdash$}}
\newcommand{\tss}{\mbox{$\models$}}
\newcommand{\qq}{\mbox{$\downarrow$}} % quasi-quote
\newcommand{\qs}{\mbox{$\prec$}}
\newcommand{\qe}{\mbox{$\succ$}}
\newcommand{\xor} {\mbox{$\dot{\vee}$}} % exclusive or
\newcommand{\radless}{\mbox{$<! \:$}}
\newcommand{\la} {\langle}
\newcommand{\ra} {\rangle}
% \newcommand{\QED} {\rule{1mm}{2.5mm}}
% \newcommand{\QED} {\framebox[0.5em][l]{\hspace{0.1em}}}
\newcommand{\QED} {\mbox{$\Box$}}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newcommand{\lleq}{\mbox{$\underline{\ll}$}}


\jairheading{10}{1999}{1-38}{4/98}{1/99}
\ShortHeadings{Order of Magnitude Comparisons of Distance}{Davis}
\firstpageno{1}


\begin{document}

\title{Order of Magnitude Comparisons of Distance}

\author{\name Ernest Davis \email davise@cs.nyu.edu \\
 \addr  Courant Institute \\ New York, NY  10012 USA}

\maketitle

\begin{abstract}
Order of magnitude reasoning --- reasoning by rough comparisons
of the sizes of quantities --- is often called ``back of the envelope 
calculation", with the implication that the calculations are quick though
approximate.  
This paper exhibits an interesting class of constraint sets in which 
order of magnitude reasoning is demonstrably fast. 
Specifically, we present a polynomial-time algorithm 
that can solve a set of constraints of the
form ``Points $a$ and $b$ are much closer together than points $c$ and $d$.''
We prove that this algorithm can be applied if 
``much closer together'' is interpreted either as referring to an infinite
difference in scale or as referring to a finite 
difference in scale, as long as the difference in scale
is greater than the number of variables in the constraint set. 
We also prove that the first-order theory over such constraints is
decidable. 
\end{abstract}

\section{Introduction}
Order of magnitude reasoning --- reasoning by rough comparisons
of the sizes of quantities --- is often called ``back of the envelope 
calculation", with the implication that the calculations are quick though
approximate.  Previous AI work on order of magnitude reasoning,
however, has focussed on its expressive power and inferential
structure, not on its computational leverage 
(Raiman, 1990; Mavrovouniotis and Stephanopoulos, 1990; Davis, 1990;
Weld, 1990).


In this paper we exhibit an interesting case where solving a set of
order of magnitude comparisons is demonstrably much faster than
solving the analogous set of simple order comparisons.
Specifically, given a set of constraints of the
form ``Points $a$ and $b$ are much closer together than points $c$ and $d$,''
the consistency of such a set can be determined in low-order polynomial time.
By contrast, it is easily shown that solving a set of constraints of the form 
``The distance from $a$ to $b$ is less than or equal to the distance
from $c$ to $d$'' in one dimension is NP-complete, and in higher dimensions
is as hard as solving
an arbitrary set of algebraic constraints over the reals.

In particular, the paper presents the following results:
\begin{itemize}
\item[1.] The algorithm ``solve\_constraints($\cal S$)'' solves a
system of constraints of the form ``Points $a$ and $b$ are infinitely
closer than points $c$ and $d$''  in polynomial time (Section 5). 
\item[2.] An improved version of the algorithm runs in time 
$O(\max(n^{2}\alpha(n)), ne, s$) where $n$ is the number of variables,
$\alpha(n)$ is the inverse Ackermann's function, 
$e$ is the number of edges mentioned in the constraint set, and $s$ is
the size of the constraint set.
(Section 6.1).
\item[3.] An extended version of the algorithm allows the inclusion 
of non-strict constraints of the form ``Points $a$ and $b$ are not
infinitely further apart than points $c$ and $d$.'' The running time
for this modified algorithm is slower than that of solve\_constraints,
but still polynomial time. (Section 6.2)
\item[4.] A different extension of the algorithm allows the combination
of order of magnitude constraints on distances with 
order comparisons on the points of the form ``Point $a$ precedes point
$b$.'' (Section 6.3)
\item[5.] The same algorithm can be applied to constraints
of the form ``The distance from $a$ to $b$ is less than $1/B$ times
the distance from $c$ to $d$,'' where $B$ is a given finite value,
as long as $B$ 
is greater than the number of variables in the constraint set. (Section 7)
\item[6.] The first-order theory over such constraints is
decidable. (Section 8)
\end{itemize}

As preliminary steps, we begin with a small example and an informal
discussion (Section 2). We then give a formal account of
order-of-magnitude spaces (Section 3)
and present a data structure called a {\em cluster tree}, which 
expresses order-of-magnitude distance comparisons (Section 4).
We conclude the paper with a discussion of the significance of these
results (Section 9).


\section{Examples}
Consider the following inferences:


\vspace{.1in}
\noindent
{\bf Example 1:}  I wish to buy a house and rent office space in a 
suburb of Metropolis.  For obvious reasons, I want the house to be close
to the school, the house to be close to the office, and the office to
be close to the commuter train station.  I am told that in Elmville
the train station is quite far from the school, but in Newton they
are close together.

{\bf Infer} that I will not be able to satisfy my constraints in Elmville,
but may be able to in Newton. 

\vspace{.1in}
\noindent
{\bf Example 2:} The Empire State Building is much closer to the Washington
Monument than to Versailles.  The Statue of Liberty is much closer
both to the Empire State Building and to Carnegie Hall than to the 
Washington Monument.

{\bf Infer} that Carnegie Hall is much closer to the Empire State Building
than to Versailles. 

\vspace{.1in}
\noindent
{\bf Example 3:}  You have to carry out a collection of computational tasks 
covering a wide range of difficulty. For instance
\begin{quote}
\begin{itemize}
\item[a.] Add up a column of 100 numbers.
\item[b.] Sort a list of 10,000 elements.
\item[c.] Invert a $100 \times 100$ matrix.
\item[d.] Invert a $1000 \times 1000$ matrix.
\item[e.] Given the O.D.E. $\ddot{x} = \cos(e^{t} x)$, $x(0)= 0$,
find $x(20)$ to 32-bit accuracy.
\item[f.] Given a online collection of 1,000 photographs in GIF format,
use state-of-the-art image recognition software to select all those
that show a man on horseback.  
\item[g.] Do a Web search until you have collected 100 pictures of 
men on horseback, using state-of-the-art image recognition software.
\item[h.] Using state-of-the-art theorem proving software, find a proof
that the medians of a triangle are concurrent.
\item[i.] Using state-of-the-art theorem proving software, find a proof
of Fermat's little theorem.
\end{itemize}
\end{quote}

It is plausible to suppose that, in many of these cases, you can say reliably
that one task will take much longer than another, either by a human
judgment or using an expert system.  For instance, task (a) is much shorter
than any of the others. Task (b) is much shorter than any of the others 
except (a) and possibly (h). 
Task (c) is certainly much shorter than (d), (f), (g), or (i).
However, with certain pairs such as (c) and (h) or (c) and (e) it would be 
difficult to guess whether one is much shorter than another, or whether
they are of comparable difficulty.

You have a number of independent identical computers, of unknown vintage
and characteristics, on which you will schedule tasks of these kinds.
Note that, under these circumstances, there is no way to predict the
absolute time required by any of these tasks within a couple of orders of 
magnitude.  Nonetheless, the comparative lengths presumably still stand.

{\bf Given:} a particular schedule of tasks on machines, infer what
you can about the relative order of completion times.
For example, given the following schedule 
\begin{quote}
Machine M1: tasks a,b,h,d. \\
Machine M2: tasks c,i.
\end{quote}
it should be possible to predict that (a) and (b) will complete before (c);
that (c) will complete before (d); and that (d) will complete before (i);
but it will not be possible to predict the order in which (c) and (h) will
complete.

In all three examples, the given information has the form ``The 
distance between points $W$ and $X$ is much less than the distance
between $Y$ and $Z$''.  In examples 1 and 2, the points are geometric.
In example 3, the points are the start and completion times of the various
tasks, and the constraints on relative lengths
can be put in the form ``The distance from 
start(a) to end(a) is much less than the distance from start(c) to end(c)'',
and so on. In example 3, there is also ordering information: the start of
each task precedes its end; the end of (a) is equal to the start of (b); and
so on.  The problem is to make inferences based on this weak kind of
constraint.


It should be noted that these 
examples are meant to be illustrative, rather than serious applications.
Example 1 does not extend in any obvious way to a class of natural, large
problems. Example 2 is implausible as a state of knowledge; how does the
reasoner find himself knowing just the order-of-magnitude relations among
distances and no other geometric information?  Example 3 is contrived. 
Nonetheless, these illustrate the
kinds of situations where order-of-magnitude relations on distance do
arise; where they express a substantial part of the knowledge of the
reasoner; and where inferences based purely on the order-of-magnitude 
comparisons can yield useful conclusions.

The methods presented in this paper involve construing the relation 
``Distance D is much shorter than distance E'' as if it were ``Distance D is
infinitesimal as compared to distance E.''  As we shall see, under this
interpretation, systems of constraints over distances can be solved 
efficiently.  The logical foundations for dealing with infinitesimal
quantities lie in the non-standard model of the real line with infinitesimals, 
developed by Abraham Robinson (1965).
(A more readable account is given by Keisler, 1976.) Reasoning with quantities
of infinitely different scale is known as ``order of magnitude'' reasoning.

The reader may ask, ``Since infinitesimals have no physical reality, what
is the value of developing techniques for reasoning about them?'' In none
of the examples, after all, is the smaller quantity truly infinitesimal
or the larger one truly infinite.  In example 1 and 2, the ratio
between successive sizes is somewhere between 10 and 100; in example 3, it is
between 100 and a rather large number difficult to estimate; but one
can always give some kind of upper bound.  It is essentially certain,
for instance, that the ratio between the times required for tasks (a) and 
(i) is less than $10^{100,000}$. Why not use the best real-valued estimate
instead?

The
first answer is that this is an idealization. Practically all 
physical reasoning and calculation rest on one idealization or another:
the idealization in the situation calculus that time is discrete; the 
idealization that solid objects are rigid, employed in most mechanics
programs; 
the idealization that such physical properties as density, temperature,
and pressure are continuous rather than local averages over atoms, which
underlies most uses of partial differential equations; the idealization 
involved in the use of the Dirac delta function; and so on.
Our idealization here that
a very short distance is infinitesimally smaller than a long
one simplifies reasoning and yields useful results  as long as care
is taken to stay within an appropriate range of application.

The second answer is that this is a technique of mathematical approximation, 
which we
are using to turn an intractable problem into a tractable one. This
would be analogous 
to linearizing a non-linear equation over a small neighborhood; or
to approximating a sum by an integral.

There are circumstances where we can be sure
that the approximation gives an answer that is guaranteed exactly correct;
namely if the actual ratio implicit in the comparison ``$D$ is much
smaller than $E$'' is larger than the number of points involved in
the system of constraints.  This will be proven in Section 7.  There
is also a broader, less well-defined, class of problems where
the approximation, though not guaranteed correct, is more reliable than
some of the other links in the reasoning.  For instance, suppose that one were
to consider an instance of example 3 involving a couple of hundred tasks,
apply order-of-magnitude reasoning, and come up with an answer that 
can be determined to be wrong.  It is possible that the error would be
due to the order-of-magnitude reasoning.  However, it seems safe to say
that, in most cases, the error is more likely to be due to a mistake in 
estimating
the comparative sizes.

\section{Order-of-magnitude spaces}

An order-of-magnitude space, or {\em om-space}, is a space of geometric
points. Any two points are separated by a distance. Two distances $d$ and 
$e$ are compared by the relation $d \ll e$, meaning ``Distance $d$ is
infinitesimal compared to $e$'' or, more loosely, ``Distance $d$ is much
smaller than $e$.'' 

For example, let $\Re^{*}$ be the non-standard real line with infinitesimals.
Let $\Re^{*m}$ be the corresponding $m$-dimensional space.  Then we can
let a point of the om-space be a point in $R^{*m}$. The distance between
two points $a,b$ is the Euclidean distance, which is a non-negative
value in $\Re^{*}$. The relation $d \ll e$ holds for two distances $d,e$,
if $d/e$ is infinitesimal.

The distance operator and the comparator are related
by a number of axioms, specified below. The most interesting of these is
called the {\em om-triangle inequality}: If $ab$ and $bc$ are both much smaller 
than $xy$, then $ac$ is much smaller than $xy$. This combines the ordinary
triangle inequality ``The distance $ac$ is less than or equal to distance
$ab$ plus distance $bc$'' together with the rule from order-of-magnitude
algebra, ``If $p \ll r$ and $q \ll r$ then $p+q \ll r$.''

It will simplify the exposition below if, rather than talking about
distances, we talk about orders of magnitude.  These are defined
as follows.  We say that two distances $d$ and $e$ have the {\em same\/}
order of magnitude if neither $d \ll e$ nor $e \ll d$. In $\Re^{*}$
this is the condition that $d/e$ is finite: neither infinitesimal
nor infinite. (Raiman, 1990 uses the notation ``$d$ Co $e$'' for this 
relation.)
By the rules of the order-of-magnitude calculus, this is an equivalence
relation. Hence we can define {\em an order of magnitude\/} to be
an equivalence class of distances under the relation ``same order of
magnitude''. For two points $a,b$, we define the function od($a,b$)
to be the order of magnitude of the distance from $a$ to $b$. 
For two orders of magnitude $p,q$, we define $p \ll q$ if, for any
representatives $d \in p$ and $e \in q$, $d \ll e$. By the rules
of the order-of-magnitude calculus, if this holds for any representatives,
it holds for all representatives. 
The advantage of using orders-of-magnitude and the function ``od'',
rather than distances and the distance function, is that it allows
us to deal with logical equality rather than the
equivalence relation ``same order of magnitude''.

For example, in the non-standard real line, let $\delta$ be a positive
infinitesimal value. Then values such as 
$\{ 1, 100, 2-50 \delta + 100 \delta^{2} \ldots \}$,
are all of the same order of magnitude, $o1$. The values
$\{ \delta, 1.001 \delta, 3 \delta + e^{- 1/\delta} \ldots
\}$ are of a different order
of magnitude $o2 \ll o1$. The values $\{ 1/\delta, 10 /\delta + \delta^{5}
\ldots \}$
are of a third order of magnitude $o3 \gg o1$.

\vspace{.1in}
\noindent
{\bf Definition 1:}
An {\em order-of-magnitude space (om-space)} $\Omega$
consists of:
\begin{itemize}
\item A set of points $\cal P$;
\item A set of orders of magnitude $\cal D$;
\item A distinguished value $0 \in \cal D$; 
\item A function ``od($a,b$)'' mapping two points $a,b \in \cal P$ to an
order of magnitude;
\item A relation ``$d \ll e$'' over two orders of magnitude $d,e \in \cal D$
\end{itemize}
satisfying the following axioms:
\begin{itemize}
\item[A.1] For any orders of magnitude $d,e \in \cal D$, exactly one of the
following holds: $d \ll e$, $e \ll d$, $d = e$.
\item[A.2] For $d,e,f \in \cal D$, if $d \ll e$ and $e \ll f$ then $d \ll f$. 
\\
(Transitivity. Together with A.1, this means that $\ll$ is a total ordering
on orders of magnitude.)
\item[A.3] For any $d \in \cal D$,  not $d \ll 0$. \\
(0 is the minimal order of magnitude.)
\item[A.4] For points $a,b \in \cal P$, od($a,b$) = 0 if and only if $a=b$. \\
(The function od is positive definite.)
\item[A.5] For points $a,b \in \cal P$, od($a,b$) = od($b,a$). \\
(The function od is symmetric.)
\item[A.6] For points $a,b,c \in \cal P$, and order of magnitude 
$d \in \cal D$, \\
if od($a,b$) $\ll$ $d$ and od($b,c$) $\ll$ $d$ then od($a,c$) $\ll$ $d$. \\
(The om-triangle inequality.)
\item[A.7] There are infinitely many different orders of magnitude.
\item[A.8] For any point $a_{1} \in \cal P$ and order of magnitude 
$d \in \cal D$,
there exists an infinite set $a_{2}, a_{3} \ldots$ such that
od($a_{i},a_{j}$) = $d$  for all $i \neq j$.
\end{itemize}


The example we have given above of an om-space, non-standard Euclidean
space, is wild and woolly and hard to conceptualize. Here are two
simpler examples of om-spaces:

I. Let $\delta$ be an infinitesimal value. We define a point to be a
polynomial in $\delta$ with integer coefficients, such as 
$3 + 5\delta - 8 \delta^{5}$. We define an order-of-magnitude to
be a power of $\delta$. We define $\delta^{m} \ll \delta^{n}$ if $m > n$;
for example, $\delta^{6} \ll \delta^{4}$. We define od($a,b$) to be
the smallest power of $\delta$ in $a-b$. For example, 
od($1+\delta^{2}-3\delta^{3}, 1-5\delta^{2}+4\delta^{4}$) = $\delta^{2}$.


II. Let $N$ be an infinite value. We define a point to be a
polynomial in $N$ with integer coefficients.
We define an order of magnitude to
be a power of $N$. We define $N^{p} \ll N^{q}$ if $p < q$;
for example, $N^{4} \ll N^{6}$. We define od($a,b$) to be
the largest power of $N$ in $a-b$. For example, 
od($1+N^{2}-3N^{3}, 1-5N^{2}+4N^{4}$) = $N^{4}$.

It can be shown that any om-space either contains a subset
isomorphic to (I) or a subset isomorphic to (II). (This is just a special
case of the general rule that any infinite
total ordering contains either an infinite descending chain or an
infinite ascending chain.)

We will use the notation ``$d \lleq e$'' as an abbreviation for 
``$d \ll e$ or $d = e$''. 

\section{Cluster Trees}

Let $P$ be a finite set of points in an om-space. If the distances between
different pairs of points in $P$ are of different orders of magnitude,
then the om-space imposes a unique tree-like hierarchical structure on $P$. 
The points will naturally fall into {\em clusters,} each cluster $C$ being a
collection of points all of which are much closer to one another than to 
any point in $P$ outside $C$. The collection of all the clusters over $P$
forms a strict tree under the subset relation.  Moreover, the structure
of this tree and the comparative sizes of different clusters in the tree
captures all of the order-of-magnitude relations between any pair of
points in $P$.  The tree of clusters is thus a very powerful data structure
for reasoning about points in an om-space, and it is, indeed, the
central data structure for the algorithms we will develop in this paper. 
In this section, we give a formal definition of cluster trees and 
prove some basic results as foundations for our algorithms.

\vspace{.1in}
\noindent
{\bf Definition 2:}
Let $P$ be a finite set of points in an om-space. A non-empty subset 
$C \subset P$
is called a {\em cluster\/} of $P$ if for every ${x,y} \in C$, 
${z} \in P-C$, od($x,y$) $\ll$ od($x,z$).  If $C$ is a cluster,
the diameter of $C$, denoted ``odiam($C$)'', is the maximum value of
od($x,y$) for ${x,y} \in C$.
\vspace{.1in}

Note that the set of
any single element of $P$ is trivially a cluster of $P$. The entire set $P$
is likewise a cluster of $P$. The empty set is by definition not a cluster
of $P$.

\vspace{.1in}
\noindent
{\bf Lemma 1:}
If $C$ and $D$ are clusters of $P$, then either $C \subset D$, $D \subset C$,
or $C$ and $D$ are disjoint.
\vspace{.1in}

\noindent
{\bf Proof:} Suppose not. Then let ${x} \in C \cap D$, 
${y} \in C-D$, ${z} \in D-C$. Since $C$ is a cluster,
od($x,y$) $\ll$ od($x,z$). Since $D$  is a cluster, od($x,z$) $\ll$ od($x,y$).
Thus we have a contradiction. $\QED$

By virtue of lemma 1, the clusters of a set $P$ form a tree.
We now develop a representation of the order of magnitude 
relations in $P$ by constructing
a tree whose nodes correspond to the clusters of $P$, labelled with
an indication of the relative size of each cluster.

\vspace{.1in}
\noindent
{\bf Definition 3:}
A {\em cluster tree} is a tree $T$ such that
\begin{itemize}
\item Every leaf of $T$ is a distinct symbol.
\item Every internal node of $T$ has at least two children.
\item Each internal node of $T$ is labelled with a non-negative value.
Two or more nodes may be given the same value. (For the purposes of
Sections 5-7, labels may be taken to be non-negative integers; in 
Section 8, it will be useful to allow rational labels.)
\item Every leaf of the tree is labelled 0.
\item The label of every internal node in the tree is less than the 
label of its parent.
\end{itemize}
\vspace{.1in}

\begin{figure}
\begin{center}
\input{omdist1-fig}
\end{center}
\caption{Cluster tree}
\label{figtree}
\end{figure}

For any node $N$ of $T$, the field ``$N$.symbols'' gives the set of symbols in
the leaves 
in the subtree of $T$ rooted at $N$, and the field ``$N$.label'' gives
the integer label on node $N$.

Thus, for example, in Figure~\ref{figtree}, n3.label=3 and n3.symbols
= $\{ a,d \}$; n1.label = 5 and n1.symbols = $\{ a,b,c,d,e,f,g \}$.

As we shall see, the nodes of the tree $T$ represent the 
clusters of a set of points, and the labels
represent the relative sizes of the diameters of
the clusters.

\vspace{.1in}
\noindent
{\bf Definition 4:}
A {\em valuation} over a set of symbols is a function mapping each symbol 
to a point in an om-space.  If $T$ is a cluster tree, a valuation over $T$
is a valuation over $T$.symbols. If $N$ is any node in $T$ and $\Gamma$
is a valuation over $T$, we will write $\Gamma(N)$ as an abbreviation
for $\Gamma$($N$.symbols).
\vspace{.1in}

We now define how a cluster tree $T$  expresses the order of magnitude
relations over a set of points $P$. 

\vspace{.1in}
\noindent
{\bf Definition 5:} 
Let $T$ be a cluster tree and 
let $\Gamma$ be a valuation over $T$.
Let $P =\Gamma(T)$, the set of points in the image of $T$ under $\Gamma$.
We say that $\Gamma \tss T$ (read $\Gamma$ {\em satisfies\/} or 
{\em instantiates} $T$)  if the following conditions hold:
\begin{itemize}
\item[i.] For any internal node $N$ of $T$, $\Gamma$($N$) is a cluster
of $P$.
\item[ii.] For any cluster $C$ of $P$, there is a node $N$ such that 
$C$=$\Gamma$($N$).
\item[iii.] For any nodes $M$ and $N$, if $M$.label $<$ $N$.label then
odiam($\Gamma$($M$)) $\ll$ odiam($\Gamma$($N$)).
\item[iv.] If label($M$) = 0, then odiam($M$) = 0. (That is, all children of
$M$ are assigned the same value under $\Gamma$.)
\end{itemize}
\vspace{.1in}

The following algorithm generates
an instantiation $\Gamma$ given a cluster tree $T$:

{\small
\begin{tabbing}
{\bf procedure} instantiate(\={\bf in} $T$ : cluster tree; 
$\Omega$ : an om-space)
\\
\> {\bf return} : array of points indexed on the symbols of $T$ \\  \\

{\bf variable} $G[N]$ : array of points indexed on the nodes of $T$; \\ \\

Let $k$ be the number of internal nodes in $T$; \\
Choose $\delta_{0} = 0 \ll \delta_{1} \ll \delta_{2} \ll \ldots \ll 
\delta_{k}$ to be
$k+1$ different orders of magnitude; \\
\> /* Such values can be chosen by virtue of axiom A.7 */ \\
pick a point $x \in \Omega$; \\
$G$[root of $T$] := $x$; \\
instantiate1($T,\Omega, \delta_{1} \ldots \delta_{k}, G$); \\
{\bf return} the restriction of $G$ to the symbols of $T$. \\
{\bf end} instantiate. \\ \\


instantiate1(\={\bf in} \=$N$ : a node in a cluster tree; 
$\Omega$ : an om-space; 
$\delta_{1} \ldots \delta_{k}$ : orders of magnitude; \\
\> {\bf in out} G : array of points indexed on the nodes of $T$) \\

{\bf if} $N$ \=is not a leaf {\bf then}\\
\> let $C_{1} \ldots C_{p}$ be the children of $N$; \\
\> ${\bf x}_{1}$ := $G[N]$; \\
\> $q$ := $N$.label; \\
\> pick \=points ${x}_{2} \ldots {x}_{p}$ such that \\
\> \>for all $i,j \in 1 \ldots p$, if $i \neq j$ then 
od(${x}_{i}, {x}_{j}$) = $\delta_{q}$; \\
\> \> /* Such points can be chosen by virtue of axiom A.8 */ \\
\> {\bf for} $i = 1 \ldots p$  do \\
\> \> $G[C_{i}]$ := ${x}_{i}$; \\
\> \> instantiate1($C_{i}, \Omega, \delta_{1} \ldots \delta_{k}, G$); \\
\> {\bf endfor} \\
{\bf endif} {\bf end} instantiate1.
\end{tabbing}
}

Thus, we begin by picking orders of magnitude corresponding to the
values of the labels. We pick an arbitrary point for the root of the tree,
and then recurse down the nodes of the tree.
For each node $N$, we place the children at points that all lie separated
by the desired diameter of $N$. The final placement of the leaves is then
the desired instantiation. 

\noindent
{\bf Lemma 2:} 
If $T$ is a cluster tree and $\Omega$ is an om-space, then 
instantiate($T,\Omega$) returns an instantiation of $T$.

The proof is given in the appendix.

Moreover, it is clear that any instantiation $\Gamma$ of $T$ can be generated
as a possible output of instantiate($T, \Omega$). 
(Given an instantiation $\Gamma$, just pick $G[N]$ at each stage
to be $\Gamma$ of some symbol of $N$.)

Note that, given any valuation $\Gamma$ over a finite set of symbols $S$,
there exists a cluster tree $T$ such that $T$.symbols = $S$ and $\Gamma$
satisfies $T$.  Such a $T$ is essentially unique up to an isomorphism over
the set of labels that preserves the label 0 and the order of labels.

\section{Constraints}
In this section, we develop the first of our algorithms. Algorithm
solve\_constraints tests a collection of constraints of the form ``$a$ is much 
closer to $b$ than $c$ is to $d$,'' for consistency.  If the set is
consistent, then the algorithm returns a cluster tree that satisfies
the constraints.  The algorithm builds the cluster tree from top to 
bottom dealing first with the large distances, and then proceeding to
smaller and smaller distances. 

Let $\cal S$ be a system of constraints of the form 
od($a,b$) $\ll$ od($c,d$); and
let $T$ be a cluster tree.  We will say that 
$T \ts {\cal S}$ (read ``$T$ satisfies $\cal S$'') 
if every instantiation of $T$ 
satisfies $\cal S$. In this section, we develop an algorithm for
finding a cluster tree that satisfies a given set of constraints.

The algorithm works along the following lines:
Suppose we have a solution satisfying $\cal S$.
Let $D$ be the diameter of the solution.
If $\cal S$ contains a constraint od($a,b$) $\ll$ od($c,d$)
then, since od($c,d$) is certainly no more than $D$, it
follows that  od($a,b$) is much smaller than $D$. We label
$ab$ as a ``short'' edge.

If two points $u$ and $v$ are connected by a path of 
short edges, then by the triangle inequality the 
edge $uv$ is also short (i.e. much shorter than $D$).
Thus, if we compute the connected components $H$ of all the
edges that have been labelled short, then all these edges in $H$
can likewise be labelled short.  For example, in table~\ref{example1-tab},
edges $vz$, $wx$, and $xy$ can all be labelled ``short''.

On the other hand, as we shall prove below, if an edge is not in the set 
$H$, then there is no reason to believe that it is much shorter than $D$.
We can, in fact, safely posit that it is the same o.m. as $D$. We label
all such edges ``long''. 

We can now assume that any connected component
of points connected by short edges is a cluster, and a child of the root
of the cluster tree. The root of the cluster tree is then given the largest
label. Its children will be given smaller labels. 
Each ``long'' edge now connects symbols in two different children of the root.
Hence, any instantiation of the tree will make any long edge longer than any
short edge.


If no edges are labelled ``long'' --- that is, if $H$ contains
the complete graph over the symbols ---
then there is an inconsistency; all edges are much shorter than
the longest edge.  For instance, in table
\ref{example2-tab}, since $vw$, $wx$, and $xy$ are all
much smaller than $zy$, it follows by the triangle inequality that 
$vy$ is much smaller than $zy$. But since we also have the 
constraints that $zy$ is much smaller than $vz$ and that $vz$
is much smaller than $vy$, we have an inconsistency. 

The algorithm then iterates, at the next smaller scale. Since we have now
taken care of all the constraints 
od($a,b$) $\ll$ od($c,d$),
where $cd$ was labelled
``long'', we can drop all those from $\cal S$.  Let $D$ now be the greatest
length of all the edges that remain in $\cal S$.
If a constraint od($a,b$) $\ll$ od($c,d$) is in the new
$\cal S$, then we know that od($a,b$) is much shorter than $D$,
and we label it ``short''.  We continue as above. The algorithm
halts when all the constraints in $\cal S$ have been satisfied,
and $\cal S$ is therefore empty; or when we encounter a contradiction, as
above.

We now give the formal statement of this algorithm.
The algorithm uses an undirected graph over the variable symbols in $\cal S$.
Given such a graph $G$, and a constraint $C$ of the form
od($a,b$) $\ll$ od($c,d$), we will refer to the edge
$ab$ as the ``short'' of $C$, and to the edge $cd$ as the ``long'' of 
$C$. The
shorts of the system $\cal S$ is the set of all shorts of the constraints of 
$\cal S$ and the longs of $\cal S$ is the set of all the longs of the 
constraints. An edge may be both a short and a long of $\cal S$ if
it appears on one side in one constraint and on the other in another 
constraint.


{\small
\begin{tabbing}
{\bf procedure} solve\_constraints(\={\bf in} $\cal S$: a system of 
constraints of the form od($a,b$) $\ll$ od($c,d$))  \\
\>{\bf return} \={\bf either} a cluster tree $T$ satisfying $\cal S$ 
if $\cal S$ is consistent; \\
\> \>{\bf or false} if $\cal S$ is inconsistent. \\ \\

{\bf type:} A node $N$ \=of the cluster tree contains \\
\>pointers to the
parent and children of $N$; \\
\> the field N.label, holding the integer label; \\
\> and the field N.symbols, holding the list of symbols in the leaves of $N$.
\\ \\

{\bf variables:} \=$m$ is an integer; \\
                 \> $C$ is a constraint in $\cal S$; \\
                 \>$H,I$ are undirected graphs; \\ 
                 \> $N,M$ are nodes of $T$; \\ \\

{\bf begin} \= {\bf if} $\cal S$ contains any constraint of the form, 
``od($a,b$) $\ll$ od($c,c$)'' {\bf then return false}; \\
\> $m$ := the number of variables in $\cal S$; \\
\> initialize $T$ to consist of a single node $N$; \\
\> $N$.symbols:= the variables in $\cal S$; \\ \\

\> {\bf repeat} 
\= $H$ := the connected components of the shorts of $\cal S$; \\
\> \> {\bf if} $H$ contains all the edges in $\cal S$
{\bf then return(false) endif}; \\
\> \> {\bf for} \=each leaf $N$ of $T$ do \\
\> \> \> {\bf if not} \=all vertices of $N$ are connected in $H$ {\bf then} \\
\> \> \> \> $N$.label := $m$; \\
\> \> \> \>{\bf for} \=each connected component $I$ of $N$.symbols in $H$ 
{\bf do} \\
\> \> \> \> \> construct node $M$ as a new child of $N$ in $T$; \\
\> \> \> \> \> $M$.symbols:= the vertices of $I$; \\
\> \> \> \>{\bf endfor} {\bf endif} {\bf endfor} \\
\> \> $\cal S$ := the subset of constraints in $\cal S$ whose long is in $H$;
\\
\> \> $m$ := $m-1$; \\
\> \> {\bf until} $\cal S$ is empty; \\ \\


\> {\bf for} each leaf $N$ of $T$ \\
\> \> $N$.label := 0; \\
\> \> {\bf if} $N$.symbols has more than one symbol \\
\> \> \> {\bf then} \=create a leaf of $N$ for each symbol in $N$.symbols; \\
\> \> \> \> label each such leaf 0; \\
\> \> \> {\bf endif} {\bf endfor} {\bf end} solve\_constraints.
\end{tabbing}
}

Tables \ref{example1-tab} and \ref{example2-tab} give two examples
of the working of procedure solve\_constraints. Table \ref{example1-tab}
shows how the procedure can be used to 
establish that the following constraints are consistent:
\begin{quote}
The Empire State Building ($x$) is much closer to the Washington Monument 
($w$) than to Notre Dame Cathedral ($v$). \\
Bunker Hill ($y$) is much closer to the Empire State Building than to the
Eiffel Tower ($z$). \\
The distance from the Eiffel Tower to Notre Dame is much less than the distance
from the Washington Monument to Bunker Hill.
\end{quote}

Table \ref{example2-tab} shows that the following inference can be justified:
\begin{quote}
{\bf Given:} The distances from the 
Statue of Liberty ($v$) to the World Trade Center ($w$), from the World
Trade Center to the Empire State Building ($x$), and from the Empire
State Building  to the Chrysler Building ($y$) are all much less than
the distance from the Chrysler Building to the Washington Monument ($z$).

{\bf Infer:} The Washington Monument is not much nearer to the Chrysler
Building than to the Statue of Liberty.
\end{quote}

This inference is carried out by asserting the negation of the consequent,
``The Washington Monument is much nearer to the Chrysler Building than
to the Statue of Liberty,'' and showing that that collection of constraints
is inconsistent.  Note that if we change ``much less'' and ``much nearer''
in this example to ``less'' and ``nearer'', then the inference
no longer valid.

\begin{table}
$\cal S$ contains the constraints
\begin{quote}
1. od($w,x$) $\ll$ od($x,v$). \\
2. od($x,y$) $\ll$ od($y,z$). \\
3. od($v,z$) $\ll$ od($w,y$). 
\end{quote}

\begin{tabbing}
The algorithm proceeds as follows: \\
Init\=ialization: \\
\> The tree is initializes to a single node with $n1$. \\
\> $n1$.symbols := \{ $v,w,x,y,z $ \}. \\ \\

Fir\=st iteration: \\
\> The shorts of $\cal S$ are \{ $wx, xy, vz$ \}. \\
\> Computing the connected components,
$H$ is set to \{ $wx, xy, wy, vz$ \}. \\
\> $n1$.label := 5; \\
\> Two \=children of $n1$ are created: \\
\> \> $n11$.symbols := ${w,x,y}$; \\
\> \> $n12$.symbols := ${v,z}$; \\
\> As $xv$ is not in $H$, delete constraint \#1 from $\cal S$. \\
\> As $yz$ is not in $H$, delete constraint \#2 from $\cal S$. \\
\> $\cal S$ now contains just constraint \#3.  \\  \\

Second iteration: \\
\> The shorts of $\cal S$ are \{ $vz$ \}. \\
\> The connected components $H$ is just $\{ vz \}$. \\
\> $n11$.label := 4; \\
\> Three children of $n11$ are created: \\
\> \> $n111$.symbols := ${w}$; \\
\> \> $n112$.symbols := ${x}$; \\
\> \> $n113$.symbols := ${z}$; \\
\> As $wy$ is not in $H$, delete constraint \#3 from $\cal S$. \\
\> $\cal S$ is now empty. \\ \\

Cleanup: \\
\> $n12$.label := 0; \\
\> Two children of $n12$ are created: \\
\> \> $n121$.symbols := ${v}$; \\
\> \> $n122$.symbols := ${z}$; \\
\end{tabbing}
(See Figure~\ref{omdist2-fig}.)
\caption{Example of computing a cluster tree}
\label{example1-tab}
\end{table}

\begin{figure}
\begin{center}
\input{omdist2-fig}
\end{center}
\caption{Building a cluster tree}
\label{omdist2-fig}
\end{figure}


\begin{table}
$\cal S$ contains the constraints
\begin{quote}
od($v,w$) $\ll$ od($z,y$). \\
od($w,x$) $\ll$ od($z,y$). \\
od($x,y$) $\ll$ od($z,y$). \\
od($z,y$) $\ll$ od($v,z$). \\
\end{quote}

\begin{tabbing}
The algorithm proceeds as follows: \\
Init\=ialization: \\
\> The tree is initializes to a single node with $n1$. \\
\> $n1$.symbols := \{ $v,w,x,y,z $ \}. \\ \\

First iteration: \\
\> The shorts of $\cal S$ are \{ $vw, wx, xy, zy, vz$ \}. \\
\> $H$ is set to its connected components, which is the complete graph over
$v,w,x,y,z$. \\
\> The algorithm exits returning {\bf false}
\end{tabbing}
\caption{Example of determining inconsistency}
\label{example2-tab}
\end{table}

Theorem 1 states the correctness of algorithm solve\_constraints.  The
proof is given in the appendix.


\noindent
{\bf Theorem 1:} 
The algorithm solve\_constraints(${\cal S}$) returns 
a cluster tree satisfying $\cal S$ if $\cal S$ is consistent, and returns 
{\bf false} if $\cal S$ is inconsistent.

There may be many cluster trees that satisfy a given set of constraints. 
Among these, the cluster tree returned by the algorithm 
solve\_constraints has an 
important property: it has the fewest possible labels consistent with
the constraints. In other words, it uses the minimum number of different
orders of magnitude of any solution. Therefore, the algorithm can be
used to check the satisfiability of a set of constraints in an om-space that
violates axiom A.7 and has only finitely many different orders
of magnitude.  If the algorithm returns $T$ and $T$ has no more
different labels than the number of different orders of magnitude in the
space, then the constraints are satisfiable. If $T$ uses more labels
than the space has orders of magnitude, then the constraints are unsatisfiable.

The proof is easier to present if we rewrite algorithm solve\_constraints
in the following form, which returns only the number of different non-zero
labels used, but does not actually construct the cluster tree.\footnote{The
reader may wonder why this simpler algorithm was not presented before the
more complicated algorithm solve\_constraints. The reason is that
the only proof we have found that the system of constraints is consistent
if num\_labels does not return {\bf false} relies on the relation
between num\_labels and the constructive solve\_constraints.}

{\small
\begin{quote}
{\bf function} num\_labels($\cal S$); \\
{\bf if} $\cal S$ is empty {\bf then return}(0) \\
{\bf else return}(1 + num\_labels(reduce\_constraints($\cal S$))) 


{\bf function} reduce\_constraints($\cal S$) \\
$H$ := connected components of the shorts of $\cal S$; \\
{\bf if} $H$ contains all the edges in $\cal S$ {\bf then return(false)} to
top-level \\
{\bf else return}(the set of constraints in $\cal S$ whose long is in $H$)
\end{quote}
}

It is easily verified that the sequence of values of $\cal S$ in 
successive recursive calls to num\_labels is the same as the sequence
of values of $\cal S$ in the main loop of solve\_constraints. Therefore
num\_labels returns the number of different non-zero labels in the tree
constructed by solve\_constraints.


\noindent
{\bf Theorem 2:} Out of all solutions to the set of constraints $\cal S$,
the instantiations of \\
solve\_constraints($\cal S$) have
the fewest number of different values of od($a,b$), where $a,b$
range over the symbols in $\cal S$. This number is given by 
num\_labels($\cal S$).

The proof is given in the appendix.

\section{Extensions and Consequences}

We next present a number of modifications of the algorithm solve\_constraints.
The first is a more efficient implementation. The second extends the algorithm
to handle non-strict comparisons.  The third extend the algorithm to handle
a combination of order-of-magnitude comparisons on distance with order
comparisons, in a one-dimensional space.

\subsection{An Efficient Implementation of Solve\_constraints}
It is possible to implement algorithm solve\_constraints somewhat more
efficiently than the naive encoding of the above description. The key
is to observe that the graph $H$ of connected components does not have
to be computed explicitly; it suffices to compute it implicitly using
merge-find sets (union-find sets). Combining this with suitable back
pointers from edges to constraints, we can formulate
a more efficient version of the algorithm.

We use the following data structures and subroutines:
\begin{itemize}
\item Each node $N$ of the cluster tree contains pointers to its parents 
and children; a field $N$.label, holding the integer label; 
a field $N$.symbols, holding the list of symbols in the leaves of $N$;
and a field $N$.mfsets, holding a list of the connected components of
the symbols in $N$.  As described below, each connected component is 
implemented as an merge-find set (MFSET). 
\item An edge $E$ in the graph over symbols contains its two endpoints,
each of which is a symbol; a field $E$.shorts, a list of the constraints
in which $E$ appears as a short; and a field $E$.longs, a list of the
constraints in which $E$ appears as a long. 
\item A constraint $C$ has two fields, $C$.short and $C$.long, both
of them edges. It also has pointers into the lists $C$.short.shorts
and $C$.long.longs, enabling $C$ to be removed in constant time 
from the constraint
lists associated with the individual edges.
\item We will use the disjoint-set forest implementation of MFSETs
(Cormen, Leiserson, and Rivest, 1990, p. 448) with merging smaller sets
into larger and path-compression. Thus, each MFSET is a upward-pointing
tree of symbols, each node of the tree being a symbol. The tree as a whole
is represented by the symbol at the root.
A symbol $A$ has then the following fields: 
\begin{itemize}
\item $A$.parent is a pointer to the parent in the MFSET tree. 
\item $A$.cluster\_leaf is a pointer to the leaf in the cluster tree containing
$A$.
\item If $A$ is the root of the MFSET then 
$A$.size holds the size of the MFSET. 
\item If $A$ is the root of the MFSET, then $A$.symbols holds all the
elements of the MFSET.
\item If $A$ is the root of the MFSET
then $A$.leaf\_ptr holds a pointer to the pointer to $A$ in $N$.mfsets
where $N$ = $A$.cluster\_leaf.
\end{itemize}
\end{itemize}


We can now describe the algorithm.

{\small
\begin{tabbing}
{\bf procedure} solve\_constraints1(\={\bf in} $\cal S$: a system of 
constraints of the form od($a,b$) $\ll$ od($c,d$)).  \\
\>{\bf return} \={\bf either} a cluster tree $T$ satisfying $\cal S$ 
if $\cal S$ is consistent; \\
\> \>{\bf or false} if $\cal S$ is inconsistent. \\ \\

{\bf variables:} \=$m$ is an integer; \\
                 \>$a,b$ are symbols; \\
                 \> $C$ is a constraint in $\cal S$; \\
                 \>$H$ is an undirected graph; \\
                 \> $E,F$ are edges; \\
                 \> $P$ is an MFSET; \\
                 \> $N,M$ are nodes of $T$; \\  \\

0. {\bf begin} \=
{\bf if} $\cal S$ contains any constraint of the form, 
``od($a,b$) $\ll$ od($c,c$)'' {\bf then return false}; \\
1.  \> $H$ := $\emptyset$; \\
2.  \>{\bf for} \=each constraint $C$ in $\cal S$ with short $E$ and long $F$
{\bf do} \\
3. \> \> add $E$ and $F$ to $H$; \\
4. \> \> add $C$ to $E$.shorts and to $F$.longs {\bf endfor}; \\
5. \>$m$ := the number of variables in $\cal S$; \\
6. \> initialize $T$ to contain the root $N$; \\
7. \> $N$.symbols := the variables in $\cal S$; \\  \\

8.\> {\bf repeat} \={\bf for} 
each leaf $N$ of $T$, INITIALIZE\_MFSETS($N$); \\
9. \> \> {\bf for} \=each edge $E=ab$ in $H$ {\bf do}  \\
10. \> \> \> {\bf if} \=$E$.shorts is non-empty and FIND($a$) $\neq$ FIND($b$)
{\bf then} \\
11. \> \> \> \> MERGE(FIND($a$), FIND($b$)) {\bf endif} {\bf endfor} \\
12. \> \> {\bf if} {\bf every} edge $E=ab$ in $H$ satisfies FIND($a$) = 
FIND($b$)
\\
13. \> \> \> {\bf then return(false) endif} \\
14. \> \> {\bf for} \=each current leaf $N$ of $T$ do \\
15. \> \> \> {\bf if} \= $N$.mfsets has more than one element {\bf then} \\
16. \> \> \> \>{\bf for} \=each mfset $P$ in $N$.mfsets {\bf do} \\
17. \> \> \> \> \> construct node $M$ as a new child of $N$ in $T$; \\
18. \> \> \> \> \> $M$.symbols:= $P$.symbols; \\
19. \> \> \> \>{\bf endfor} {\bf endif} {\bf endfor} \\
20. \> \> {\bf for} each edge $E = ab$ in $H$ {\bf do} \\
21. \> \> \> {\bf if} FIND($a$) $\neq$ FIND($b$) {\bf then} \\
22. \> \> \> \> {\bf for} each constraint $C$ in $E$.longs {\bf do} \\
23. \> \> \> \> \> delete $C$ from $\cal S$; \\
24. \> \> \> \> \> delete $C$ from $E$.longs; \\
25. \> \> \> \> \> delete $C$ from $C$.short.shorts {\bf endfor} \\
26. \> \> \> \> delete $E$ from $H$ {\bf endif} {\bf endfor} \\
27. \> \> $m$ := $m-1$; \\
28. \> \> {\bf until} $\cal S$ is empty; \\ \\


29. \> {\bf for} each leaf $N$ of $T$ \\
30. \> \> $N$.label := $0$; \\
31. \> \> {\bf if} $N$.symbols has more than one symbol \\
32. \> \> \> {\bf then} create a leaf of $N$ with label 0
for each symbol in $N$.symbols; \\
33. \> \> \> {\bf endif} {\bf endfor} {\bf end} solve\_constraints1. 
\end{tabbing}


\begin{tabbing}
{\bf procedure} INITIALIZE\_MFSETS($N$ : node) \\
{\bf var} \=$A$ : symbol; \\
$N$.mfsets := $\emptyset$; \\
{\bf for} $A$ in $N$.symbols {\bf do} \\ 
\> $A$.parent := null; \\ 
\> $A$.cluster\_leaf := $N$; \\ 
\> $A$.symbols := $\{ A \}$; \\ 
\> $A$.size := 1; \\ 
\> $N$.mfsets := cons($A$,$N$.mfsets); \\
\> $A$.leaf\_ptr := $N$.mfsets; \\
{\bf endfor}  {\bf end} INITIALIZE\_MFSETS. \\ \\

{\bf procedure} MERGE({\bf in} $A,B$ : symbol) \\
{\bf if} $A$.size $>$ $B$.size {\bf then} swap($A,B$); \\
$A$.parent := $B$; \\
$B$.size := $B$.size + $A$.size; \\
$B$.symbols := $B$.symbols $\cup$ $A$.symbols; \\
Using $A$.leaf\_ptr, delete $A$ from $A$.cluster\_leaf.mfsets; \\
{\bf end} MERGE. \\ \\

{\bf procedure} FIND({\bf in} $A$ : symbol) {\bf return} symbol; \\
{\bf var} $R$ : symbol; \\
{\bf if} $A$.parent = null {\bf then} {\bf return} $A$ \\
\> {\bf else} \=$R$ := FIND($A$.parent); \\
\> \> $A$.parent := $R$;    /* Path compression */ \\
\> \> {\bf return}($R$) \\
{\bf end} FIND.
\end{tabbing}
}

Let $n$ be the number of symbols in $\cal S$; let $e$ be the number of
edges; and let $s$ be the number of constraints.  Note that 
$n/2 \leq e \leq n(n-1)/2$ and that $e/2 \leq s \leq e(e-1)/2$. 
The running time of solve\_constraints1 can be computed as follows.
As each iteration of the main loop 8-28 splits at least one of
the connected components of $H$, there can be at most $n-1$ iterations.
The MERGE-FIND operations in the {\bf for} loop 9-11 take together time at most
$O(\max(n \alpha(n), e))$ where $\alpha(n)$ is the inverse Ackermann's
function. Each iteration of the inner {\bf for} loop lines 16-18 creates
one node $M$ of the tree. Therefore, there are only $O(n)$ iterations
of this loop over the entire algorithm. Lines 14,
15 of the outer {\bf for} loop require at most $n$ iterations in each iteration
of the main loop. 
The {\bf for} loop 22-26 is executed exactly once in the course of
the entire execution of the algorithm for each constraint $C$, and hence
takes at most time $O(s)$ over the entire algorithm.  Steps 20-21 require
time $O(e)$ in each iteration of the main loop. 
It is easily verified
that the remaining operations in the algorithm take no more time than
these.  Hence the overall running time is O($\max(n^{2}\alpha(n), ne, s))$.

\subsection{Adding Non-strict Comparisons}

The algorithm solve\_constraints can be modified to deal with
non-strict comparisons of the form od($a,b$) $\lleq$ od($c,d$) 
by, intuitively, marking the edge $ab$ as ``short'' on each iteration
if the edge $cd$ has been found to be short. 

Specifically, in algorithm solve\_constraints, we make the following two
changes. First, the revised algorithm takes two parameters: $\cal S$, the set 
of strict
constraints, and $\cal W$, the set of non-strict constraints. Second, we
replace the line

{\small
\begin{quote}
$H$ := the connected components of the shorts of $\cal S$ \\
\end{quote}
}
with the following code:

{\small
\begin{tabbing}
1. \hspace{1em} \=$H$ := the shorts of $\cal S$; \\
2. \> {\bf repeat} \=$H$ := the connected components of $H$; \\
3. \> \> {\bf for} \=each weak constraint od($a,b$) $\lleq$ od($c,d$)  \\
4. \> \> \>{\bf if} $cd$ is in $H$ then add $ab$ to $H$  
{\bf endif endfor} \\
5. \>{\bf until} no change has been made to $H$ in the last iteration.
\end{tabbing}
} 


The proof that the revised algorithm is correct 
is only a slight extension of the
proof of  theorem 1 and is given in the appendix.

Optimizing this algorithm for efficiency is a little involved, not only
because of the new operations that must be included, but also because
there are now four parameters --- $n$, the number of symbols; $e$, the
number of edges mentioned; $s$, the number of strict comparison; and
$w$, the number of non-strict comparisons --- and the optimal implementation
varies depending on their relative sizes. In particular, either $s$ or
$w$, though not both, may be much smaller than $n$, and each of these
cases requires special treatment for optimal efficiency.  The best
implementation we have found for the case where both $s$ and $w$ are
$\Omega(n)$ has a running time of O($\max(n^{3}, nw, s)$). The details
of the implementation are straightforward and 
not of sufficient interest to be worth 
elaborating here.

An immediate consequence of this result is that a couple of problems of
inference are easily computed:
\begin{itemize}
\item To determine whether a constraint $C$ is the consequence of a 
set of constraints $\cal S$, form the set  ${\cal S} \cup \neg C$
and check for consistency.  If ${\cal S} \cup \neg C$ is 
inconsistent then ${\cal S} \tss C$. Note that the negation of
the constraint od($a,b$) $\ll$ od($c,d$) is the constraint \\
od($c,d$) $\lleq$ od($a,b$).
\item To determine whether two sets of constraints are logically equivalent, 
check that each constraint in the first is a consequence of the second,
and vice versa.
\end{itemize}

\subsection{Adding Order Constraints}
Example 3 of Section 2 involves a combination of order-of-magnitude
constraints on distances together with simple ordering on points, where
the points lie on a one-dimensional line.  We next show how to extend
algorithm solve\_constraints to deal with this more complex situation.

In terms of the axiomatics, adding an ordering on points involves
positing that the relation $p < q$ is a total ordering and that
the ordering of points is related to order of magnitude comparisons
of distances through the following axiom.
\begin{itemize}
\item[A.9] For points $a,b,c \in {\cal P}$, if $a < b < c$ 
then od($a,b$) $\lleq$ od($a,c$).
\end{itemize}
The following rule is easily deduced: If $C$ and $D$ are disjoint clusters,
then either every point in $C$ is less than all the points in $D$, or
vice versa.


In extending our algorithm, we begin by defining an {\em ordered cluster
tree} to be a cluster tree where, for every internal node $N$, there
is a partial order on the children of $N$.  If $A$ and $B$ are children
of $N$ and $A$ is ordered before $B$, then in an instantiation of the tree,
every leaf of $A$ must precede every leaf of $B$. Procedure instantiate1
can then be modified to deal with ordered cluster trees as follows:

{\small
\begin{tabbing}
instantiate1(\={\bf in} \=$N$ : a node in a cluster tree; 
$\Omega$ : an om-space; 
$\delta_{1} \ldots \delta_{k}$ : orders of magnitude; \\
\> {\bf in out} G : array of points indexed on the nodes of $T$) \\

{\bf if} $N$ \=is not a leaf {\bf then}\\
\> let $C_{1} \ldots C_{p}$ be the children of $N$ in topologically sorted
order; \\
\> ${\bf x}_{0}$ := $G[N]$; \\
\> $q$ := $N$.label; \\
\> pick \=points ${x}_{1} \ldots {x}_{p}$ in increasing order such that \\
\> \>for all $i,j \in 0 \ldots p$, if $i \neq j$ then 
od(${x}_{i}, {x}_{j}$) = $\delta_{q}$; \\
\> \> /* Such points can be chosen by virtue of axiom A.8 */ \\
\> {\bf for} $i = 1 \ldots p$  do \\
\> \> $G[C_{i}]$ := ${x}_{i}$; \\
\> \> instantiate1($C_{i}, \Omega, \delta_{1} \ldots \delta_{k}, G$) \\
\> {\bf endfor} \\
{\bf endif} {\bf end} instantiate1.
\end{tabbing}
}

Algorithm solve\_constraints is modified as follows:
{\small
\begin{tabbing}
{\bf procedure} solve\_constraints2(\={\bf in} \=$\cal S$: a system of 
constraints of the form od($a,b$) $\ll$ od($c,d$) ; \\
\{NEW\} \> \>$\cal O$ : a system of constraints of the form $a < b$) \\
\>{\bf return} \={\bf either} an \=ordered cluster tree $T$ satisfying 
$\cal S$ \\
\> \> \>if $\cal S$ is consistent; \\
\> \>{\bf or false} if $\cal S$ is inconsistent. \\ \\


{\bf variables:} \=$m$ is an integer; \\
                 \> $C$ is a constraint in $\cal S$; \\
                 \>$H,I$ are undirected graphs; \\ 
                 \> $M,N,P$ are nodes of $T$; \\ 
                 \> $a,b,c,d$ are symbols; \\ \\

{\bf begin} \hspace{.5em}\= {\bf if} 
\=$\cal S$ contains any constraint of the form, 
``od($a,b$) $\ll$ od($c,c$)'' \\
\> \>{\bf then return false}; \\
\{NEW\}\> {\bf if} $\cal O$ is internally inconsistent (contains a cycle) 
{\bf then return false}; \\
\> $m$ := the number of variables in $\cal S$; \\
\> initialize $T$ to consist of a single node $N$; \\
\> $N$.symbols:= the variables in $\cal S$; \\ \\

\> {\bf repeat} \= $H$ := the connected component of the shorts of $\cal S$; \\
\{NEW\}\> \>  $H$ := incorporate\_order($H, \cal O$); \\     
\> \> {\bf if} $H$ contains all the edges in $\cal S$ 
{\bf then return false} \\ \\

\> \> {\bf for} \=each leaf $N$ of $T$ do \\
\> \> \> {\bf if not} \=all vertices of $N$ are connected in $H$ {\bf then} \\
\> \> \> \> $N$.label := $m$; \\
\> \> \> \>{\bf for} \=each connected component $I$ of $N$.symbols in $H$ 
{\bf do} \\
\> \> \> \> \> construct node $M$ as a new child of $N$ in $T$; \\
\> \> \> \> \> $M$.symbols:= the vertices of $I$; \\
\> \> \> \>{\bf endfor} {\bf endif} \\
\{NEW\}\> \> \> {\bf for} each constraint $a < b \in {\cal O}$ \\
\{NEW\}\> \> \> \> {\bf if} \=$a$ is \=in $M$.symbols and $b$ is in 
$P$.symbols \\
\{NEW\} \> \> \> \> \> \>where $M$ and $P$ are different children of $N$ \\
\{NEW\}\> \> \> \> \> {\bf then} add an ordering arc from $M$ to $P$; \\
\{NEW\}\> \> \> \> {\bf endif endfor} \\
\> \> {\bf  endfor} \\ \\

\> \> $\cal S$ := the subset of constraints in $\cal S$ whose long is in $H$;
\\
\> \> $m$ := $m-1$; \\
\> \> {\bf until} $\cal S$ is empty; \\ \\


\> {\bf for} each leaf $N$ of $T$ \\
\> \> $N$.label := 0; \\
\> \> {\bf if} $N$.symbols has more than one symbol \\
\> \> \> {\bf then} \=create a leaf of $N$ for each symbol in $N$.symbols; \\
\> \> \> \> label each such leaf 0; \\
\> \> \> {\bf endif} {\bf endfor} \\
{\bf end} solve\_constraints2. \\ \\
\end{tabbing}


\begin{tabbing}
\{NEW\} \\
{\bf function} incorporate\_order(\={\bf in} \=$H$ : undirected graph; \\ 
\> \> $\cal O$ : a system of constraints of the form $a < b$) \\ 
\> {\bf return} undirected graph; \\ \\

{\bf variables:} \= $G$ : directed graph; \\
\> $a,b$ : vertices in $H$; \\
\> $A,B$ : connected components of $H$; \\
\> $V[A]$ : {\bf array} of vertices of $G$ indexed on connected components 
of $H$; \\
\> $I$ : subset of vertices of $G$; \\
\\ \\

{\bf for each} connected component $A$ of $H$ create a vertex $V[A]$ in $G$; \\
{\bf for each} \=constraint $a < b \in \cal O$  \\
 \> let $A$ and $B$ be the connected components of $H$ containing 
$a$ and $b$ respectively; \\
\> {\bf if} $A \neq B$ {\bf then} add an arc in $G$ from $V[A]$ to
$V[B]$ {\bf endif endfor}; \\
{\bf for each} strongly connected component $I$ of $G$ {\bf do} \\
\> {\bf for each} \=pair of distinct vertices $V[A], V[B] \in I$ {\bf do} \\
\> \> {\bf for each} $a \in A$ and $b \in B$ add the edge $ab$ to $H$ 
{\bf endfor endfor} \\
{\bf endfor} \\
{\bf end} incorporate\_order.
\end{tabbing}
}

Function incorporate\_order serves the following purpose. Suppose that
we are in the midst of the main loop of solve\_constraints2, we have
a partially constructed cluster tree, and we are currently working
on finding the sub-clusters of a node $N$.  As in the original form
of solve\_constraints, we find the connected components of the shorts of
the order-of-magnitude constraints.  Let these be $C_{1} \ldots C_{q}$;
then we know that the diameter of each $C_{i}$ is much smaller than
the diameter of $N$.  Now, suppose, for example, that we have
in $\cal O$ the constraints $a_{1} < a_{5}, b_{5} < b_{2}, c_{2} < c_{1}$,
where $a_{1}, c_{1} \in C_{1};$ $b_{2}, c_{2} \in C_{2}$; and $a_{5}, b_{5}
\in C_{5}$.  Then it follows from axiom A.9 that $C_{1}$, $C_{2}$, and $C_{5}$ 
must all be merged into a single cluster, whose diameter will be less
than the diameter of $N$.   Procedure incorporate\_order finds all such
loops by constructing a graph $G$ whose vertices are the connected components
of $H$ and whose arcs are the ordering relations in $\cal O$ and then
computing the strongly connected components of $G$. (Recall that two
vertices $u,v$ in a directed graph are in the same strongly connected component
if there is a cycle from $u$ to $v$ to $u$.)  It then merges together
all of the connected components of $H$ that lie in a single strongly
connected component of $G$.

The proof of the correctness of algorithm solve\_constraints2 is again
analogous in structure to the proof of theorem 1, and is given in the appendix.


By implementing this in the manner of Section 6.1, the algorithm can
be made to run in time
$O(\max(n^{2}\alpha(n), ne, no, s))$, where $o$ is the number of constraints
in $\cal O$.


\section{Finite order of magnitude comparison}

In this section, it is demonstrated that algorithm solve\_constraints
can be applied to systems of constraints of the form 
``dist($a,b$) $<$ dist($c,d$) / $B$'' for finite $B$ in ordinary Euclidean
space as long as
the number of symbols in the constraint network is smaller than $B$.

We could be sure immediately that some such result must apply for finite
$B$. It is a fundamental property of the non-standard real line that any
sentence in the first-order theory of the reals that holds for all infinite
values holds for any sufficiently large finite value, and that any sentence
that holds for some infinite value holds for arbitrarily large finite values.
Hence, since the answer given by algorithm solve\_constraints works over a 
set of
constraints $\cal S$ when the constraint ``od($a,b$) $\ll$ od($c,d$)''
is interpreted as ``od($a,b$) $<$ od($c,d$)/$B$ for infinite $B$'', the
same answer must be valid for sufficiently large finite $B$.  What is 
interesting is that we can find a simple characterization of $B$ in 
terms of $\cal S$; namely, that $B$ is larger than the number of symbols
in $\cal S$.

We begin by modifying the form of the constraints, and the 
interpretation of a cluster tree. 
First, to avoid confusion, we will use a four-place predicate 
``much\_closer($a,b,c,d$)'' rather than the form ``od($a,b$) $\ll$ od($c,d$)''
as we are not going to give an interpretation to ``od'' as a function.
We fix a finite value $B > 1$, and interpret ``much\_closer($a,b,c,d$)''
to mean ``dist($a,b$) $<$ dist($c,d$) / $B$.''

We next redefine what it means for a valuation to instantiate a cluster
tree:

\vspace{.1in}
\noindent
{\bf Definition 6:} Let $T$ be a cluster tree and let $\Gamma$ be a valuation
on the symbols in $T$. We say that $\Gamma \ts T$ if the following holds:
For any symbols $a,b,c,d$ in $T$, let $M$ be the least common ancestor of $a,b$
and let $N$ be the least common ancestor of $c,d$. If $M$.label $<$ $N$.label
then much\_closer($a,b,c,d$).
\vspace{.1in}

Procedure ``instantiate'', which generates an instantiation of a cluster
tree, is modified as follows:


{\small
\begin{tabbing}
{\bf procedure} instantiate(\={\bf in} $T$ : cluster tree; 
$\Omega$ : Euclidean space; $B$ : real);
\\
\> {\bf return} : array of points indexed on the symbols of $T$; \\  \\

Let $n$ be the number of nodes in $T$; \\
$\alpha$ := $2 + 2n + Bn$; \\
Choose $\delta_{1}, \delta_{2} \ldots \delta_{n}$ 
such that $\delta_{i} < \delta_{i+1} / \alpha$; \\
pick a point $x \in \Omega$; \\
$G[T] := x$; \\
instantiate1($T,\Omega, \delta_{1} \ldots \delta_{n}, G$); \\
{\bf return} the restriction of $G$ to the symbols of $T$. \\
{\bf end} instantiate. \\ \\


instantiate1(\={\bf in} \=$N$ : a node in a cluster tree; 
$\Omega$ : a Euclidean space; \\
\> \> $\delta_{1} \ldots \delta_{n}$ : orders of magnitude; \\
\> {\bf in out} G : array of points indexed on the nodes of $T$) \\

{\bf if} $N$ \=is not a leaf {\bf then}\\
\> let $C_{1} \ldots C_{p}$ be the children of $N$; \\
\> ${\bf x}_{1}$ := $G[N]$; \\
\> $q$ := $N$.label; \\
\> pick \=points ${x}_{2} \ldots {x}_{p}$ such that \\
\> \>for all $i,j \in 1 \ldots p$, if $i \neq j$ then 
$\delta_{q}$ $\leq$ dist(${x}_{i}, {x}_{j}$) $<$ $n \delta_{q}$ \\
\> /* This is possible since $p \leq n$. */ \\
\> {\bf for} $i = 1 \ldots p$  do \\
\> \> $G[C_{i}]$ := ${x}_{i}$; \\
\> \> instantiate1($C_{i}, \Omega, \delta_{1} \ldots \delta_{n}, G$) \\
\> {\bf endfor} \\
{\bf endif} {\bf end} instantiate1.
\end{tabbing}
}

The analogue of lemma 2 holds for the revised algorithm:

\noindent
{\bf Lemma 22:} Any cluster tree $T$ has an instantiation in  Euclidean 
space $\Re^{m}$ of any dimensionality $m$.

We can now state theorem 3, which asserts the correctness of algorithm
``solve\_constraints'' in this new setting:

\vspace{.1in}
\noindent

{\bf Theorem 3:} Let $\cal S$ be a set of constraints over $n$ variables
of the form ``dist($a,b$) $<$ dist($c,d$) / $B$'', where $B > n$. 
The algorithm solve\_constraints(${\cal S}$) returns 
a cluster tree satisfying $\cal S$ if $\cal S$ is consistent over Euclidean 
space, and returns 
{\bf false} if $\cal S$ is inconsistent.


The proofs of lemma 22 and theorem 3  are given in the appendix.

An examination of the proof of lemma 22 shows that this result does not
depend on any relation between $n$ and $B$. 
Therefore, if solve\_constraints($\cal S$) returns a tree $T$, then 
$\cal S$ is consistent and $T$ satisfies $\cal S$ regardless of the relation
between $n$ and $B$. However, it is possible for $\cal S$ to be consistent
and solve\_constraints($\cal S$) to return {\bf false} if $n \geq B$. 
On the other hand, one can see from the proof of theorem 3 (particularly
lemma 23) that
if $B > n$ and solve\_constraints($\cal S$) returns {\bf false} 
then $\cal S$ is inconsistent in any metric space. However, there
are metric spaces other than $\Re^{m}$ in which the cluster tree
returned by solve\_constraints may have no instantiation. 


\section{The first-order theory}

Our final result asserts that if the om-space is rich enough
then the full first-order language
of order-of-magnitude distance comparisons is decidable. Specifically,
if the collection of orders of magnitude is dense and unbounded above,
then there is a decision algorithm for first-order sentences over
the formula, ``od($W,X$) $\ll$ od($Y,Z$)'' that runs in time 
$O(4^{n} (n!)^{2} s)$ where $n$ is the number of variables in the sentence
and $s$ is the length of the sentence. 

The basic reason for this is the following: As we have observed in
corollary 4, a cluster tree $T$ determines the truth value of all 
constraints of the form ``od($a,b$) $\ll$ od($c,d$)'' where $a,b,c,d$
are symbols in the tree. That is, any two instantiations of $T$ in
any two om-spaces agree on any such constraint. If we 
further require that the om-spaces are dense and unbounded, then 
a much stronger statement holds: Any two instantiations of $T$ over such
om-spaces agree
on {\em any\/} first-order formula free in the symbols of $T$ over the relation 
``od($W,X$) $\ll$ od($Y,Z$)''.  Hence, it suffices to check the truth of 
a sentence over all possible cluster trees on the variables in the sentence.
Since there are only finitely many cluster trees over a fixed set of
variables (taking into account only the relative order of the labels
and not their numeric values), this is a decidable procedure.

Let $\cal L$ be the first-order language with equality with no constant
or function symbols, and the single predicate symbol 
``much\_closer($a,b,c,d$)''.  It is easily shown 
that $\cal L$
is as expressive as the language with the function symbol ``od'' and the
relation symbol $\ll$. 

\vspace{.1in}
{\bf Definition 7:} An om-space $\Omega$ with orders of magnitude $\cal D$
is {\em dense} if it
satisfies the following axiom:
\begin{itemize}
\item[A.9] For all orders of magnitude $\delta_{1} \ll \delta_{3}$ in 
$\cal D$, there exists a order of magnitude $\delta_{2}$ in $\cal D$ such that
$\delta_{1} \ll \delta_{2} \ll \delta_{3}$.
\end{itemize}
$\Omega$ is {\em unbounded above} if it satisfies the following:
\begin{itemize}
\item[A.10] For every order of magnitude $\delta_{1}$ in $\cal D$ there
exists $\delta_{2}$ in $\cal D$ such that $\delta_{1} \ll \delta_{2}$.
\end{itemize}
\vspace{.1in}

If $\cal D$ is the collection of orders of magnitude in the hyperreal line,
then both of these are satisfied. In axiom [A.9], 
if $0 \ll \delta_{1} \ll \delta_{3}$, choose $\delta_{2} = 
\sqrt{\delta_{1} \delta_{3}}$, the geometric mean. If 
$0 = \delta_{1} \ll \delta_{3}$, choose $\delta_{2} = \delta_{3} \delta$
where $\delta \ll 1$. In axiom [A.10] choose $\delta_{2} = \delta_{1} / \delta$
where $0 < \delta \ll 1$.

\vspace{.1in}
{\bf Definition 8:} Let $T$ be a cluster tree. Let $l_{0}=0, l_{1}, l_{2} 
\ldots l_{k}$
be the distinct labels in $T$ in ascending order.
An {\em extending label} for 
$T$ is either (a) $l_{i}$ for some $i$; (b) $l_{k}+1$ (note that $l_{k}$ is
the label of the root); (c) $(l_{i-1} + l_{i})/2$ for some $i$ between 1 and 
$k$. 
\vspace{.1in}

Note that if $T$ has $k$ distinct non-zero labels, then there are 
$2k+2$ different extending labels for $T$.

\vspace{.1in}
{\bf Definition 9:} Let $T$ be a cluster tree.
Let $x$ be a symbol not in $T$. The cluster tree $T^{\prime}$ {\em extends
$T$ with $x$} if $T^{\prime}$ is formed from $T$ by applying one of
the following operations (a single application of a single operation).
\begin{itemize}
\item[1.] $T$ is the null tree and $T^{\prime}$ is the tree containing
the single node $x$.
\item[2.] $T$ consists of the single node for symbol $y$. Make a new node
$M$, make both $x$ and $y$ children of $M$, and set the label of $M$ to
be either 0 or 1.
\item[3.] For any internal node $N$ of $T$ (including the root), make $x$
a child of $N$.
\item[4.] Let $y$ be a symbol in $T$, and let 
$N$ be its father. If
$N$.label $\neq$ 0, create a new node $M$ with an extending label for $T$
such that $M$.label $<$ $N$.label. Make $M$ a child of $N$, and make
$x$ and $y$ children of $M$.
\item[5.] Let $C$ be an internal node of $T$ other than the root, 
and let $N$ be its father.
Create a new node $M$ with an extending label for $T$ such that
$C$.label $<$ $M$.label $<$ $N$.label. Make $M$ a child of $N$ and make
$x$ and $C$ children of $M$.
\item[6.] Let $R$ be the root of $T$. Create a new node $M$ such that
$M$.label = $R$.label + 1. Make $R$ and $x$ children of $M$. Thus $M$
is the root of the new tree $T^{\prime}$.
\end{itemize}
(See Figure ~\ref{figextension}.)
\vspace{.1in}

\begin{figure}
\begin{center}
\input{omdist3-fig}
\end{center}
\caption{Extensions of a cluster tree}
\label{figextension}
\end{figure}

Note that if $T$ is a tree of $n$ symbols and at most $n-1$ internal nodes then
\begin{itemize}
\item There are $n-1$ ways to carry out step 3.
\item There are $n$ possible ways to choose symbol $y$ in step 4, and 
at most $2n-2$ for the label on $M$ in each.
\item There are at most $n-2$ different choices for $C$ in step 5,
and at most $2n-3$ choices for the label on $M$ in each.
\item There is only one way to carry out step 6.
\end{itemize}

Hence, there are less than $4 n^{2}$ different extensions of $T$ by $x$.
(This is almost certainly an overestimate by at least a factor of 2,
but the final algorithm is so entirely impractical that it is
not worthwhile being more precise.)


\vspace{.1in}
\noindent
{\bf Definition 10:} Let $T$ be a cluster tree, and let $\phi$ be a formula
of $\cal L$ open in the variables of $T$. $T$ {\em satisfies} $\phi$ if every
instantiation of $T$ satisfies $\phi$. 


\vspace{.1in}
\noindent
{\bf Theorem 4:} Let $T$ be a cluster tree. Let $\phi$ be an open formula
in $\cal L$, whose free variables are the symbols of $T$. 
Let $\Omega$ be an om-space
that is dense and unbounded above. Algorithm decide($T,\phi$) returns
{\bf true} if $T$ satisfies $\phi$ and {\bf false} otherwise.
\vspace{.1in}

{\small
\begin{tabbing}
{\bf function} decide($T$ : cluster tree; $\phi$ : formula) {\bf return boolean}
\\
convert \=$\phi$ to an \=equivalent form  in which 
 the only logical symbols in $\phi$ are \\
\> \>$\neg$ (not), $\wedge$ (and),
$\te$ (exists), = (equals) and variable names, \\
\> and the only non-logical
symbol is the predicate ``much\_closer''. \\
{\bf case} \= \\
\> $\phi$ has form $X=Y$: {\bf return} (distance($X,Y,T$) = 0); \\
\> $\phi$ has form ``much\_closer($W,X,Y,Z$)'': {\bf return} 
distance($W,X,T$) $<$ distance($Y,Z,T$)); \\ 
\> $\phi$ has form $\neg \psi$: {\bf return not}(decide($T,\psi$)) \\
\> $\phi$ has form $\psi \wedge \theta$: {\bf return}(decide($T,\psi$) 
{\bf and} decide($T,\theta$)) \\
\> $\phi$ \=has \=form $\te_{X} \alpha$;  \\
\> \> {\bf if for some} extension $T^{\prime}$ of $T$ by $X$, 
decide($T^{\prime},\alpha$) = {\bf true} \\
\> \> \> {\bf then return true} \\
\> \> \> {\bf else return false endif endcase} \\
{\bf end} decide \\ \\

{\bf function} distance($X,Y$ : symbol; $T$ : cluster tree) {\bf return 
integer} \\
$N$ := the common ancestor of $X$ and $Y$ in $T$; \\
{\bf return}($N$.label)  \\
{\bf end} distance
\end{tabbing}
}

The proof of theorem 4 is given in the appendix.

Running time: As we have remarked above, for a tree $T$ of size $k$ there
are at most $4k^{2}$ extensions of $T$ to be considered. The total
number of cluster trees considered is therefore bounded by
$\Pi_{k=1}^{n} 4k^{2}$ = $4^{n} (n!)^{2}$.  It is easily verified that the
logical operators other than quantifiers add at most a factor of $s$ where
$s$ is the length of the sentence. Hence the running time is bounded
by $O(4^{n} (n!)^{2} s)$.

A key lemma, of interest in itself, states the following:

\noindent
{\bf Lemma 28:} Let $T$ be a cluster tree. Let $\phi$ be an open formula
in $\cal L$, whose free variables are the symbols of $T$. 
Let $\Omega$ be an om-space
that is dense and unbounded above. 
If one instantiation $\Gamma$ of $T$ in $\Omega$ satisfies $\phi$ then every 
instantiation of $T$ in $\Omega$ satisfies $\phi$.

That is, either $\phi$ is true for all instantiations of $T$ or for none.
The proof is given in the appendix.  

It should be observed that the above conditions on $\Omega$ in lemma 28
are necessary, and that the statement is false otherwise.  For example,
let $\Omega$ be the om-space described in example I, Section 3, of
polynomials over an infinitesimal $\delta$. Then $\Omega$ is not
unbounded above; there is a maximum order-of-magnitude $O(1)$. 
Let $T$ be the starting tree of Figure 3 (upper-left corner).
Let $\phi$ be the formula ``$\te_{X}$ od($V,W$) $\ll$ 
od($W,X$)'', free in $V$ and $W$. Then the valuation 
$\{  U \rightarrow \delta, V \rightarrow 0,
W \rightarrow 1 \}$ satisfies $T$ but not $\phi$, whereas the valuation
$\{ U \rightarrow \delta^{2}, V \rightarrow 2 \delta^{2},
W \rightarrow \delta \}$ satisfies both $T$ and $\phi$.

\section{Conclusions}
The applications of the specific algorithms above are undoubtedly limited;
we are not aware of any practical problems where solving systems of
order-of-magnitude relations on distances is the central problem.  However,
the potential applications of order-of-magnitude reasoning generally are very 
widespread.  Ordinary commonsense reasoning involves distances spanning 
a ratio of about $10^{8}$, from a fraction of an inch to thousands of miles,
and durations spanning a ratio of about $10^{10}$, from a fraction of a second
to a human lifetime.  Scientific reasoning spans much greater ranges.
Explaining the dynamics of a star combines reasoning about nuclear 
reactions with reasoning about the star as a whole; these differ by 
a ratio of about $10^{57}$.  The techniques needed to compute with quantities
of such vastly differing sizes are quite different from the techniques 
needed to compute with quantities all of similar sizes.  This paper is a
small step in the development and analysis of such computational techniques.

The above results are also significant in the encouragement that
they give to the hope that order-of-magnitude reasoning specifically, and
qualitative reasoning generally, may lead to useful quick reasoning 
strategies in a broader range of problems.  It has been often found in AI
that moving from greater to lesser precision in the mode of inference or type 
of knowledge does not lead to quick and dirty heuristic techniques, but
rather to slow and dirty techniques.  Nonmonotonic reasoning is the
most notorious example of this, but it arises as well in many other types
of automated reasoning, including qualitative spatial and physical
reasoning.  The algorithms developed in this paper are a welcome exception
to this rule.  We are currently studying algorithmic techniques for
other order-of-magnitude problems, and are optimistic of finding similar
favorable results.

\section*{Acknowledgements}
This research has been supported by
NSF grant \#IRI-9625859.  Thanks to Ji-Ae Shin, Andrew Gelsey, and the
reviewers for helpful comments.

\section*{Appendix A. Proofs}

In this appendix, we give the proofs of the various results asserted in
the body of the paper.

\subsection*{Proof of Lemma 2}

\vspace{.1in}
\noindent
{\bf Lemma 2:} 
If $T$ is a cluster tree and $\Omega$ is an om-space, then 
instantiate($T,\Omega$) returns an instantiation of $T$.

\vspace{.1in}
\noindent
{\bf Proof:} Let $\delta_{0} = 0$. 
For any node $N$, if $i$=$N$.label, we define
$\Delta(N) = \delta_{i}$. The proof then proceeds in the following 
steps:

\begin{itemize}
\item[i.] For any nodes $M$,$N$, if $M$ is a descendant of $N$ in $T$ then 
od($G[M],G[N]$) $\lleq$ $\Delta(N)$. 
{\bf Proof:} If $M$ is a child of $N$,
then this is immediate from the construction of 
${x}_{2} \ldots {x}_{p}$ in instantiate1. Else, let 
$N=N_{1}, N_{2} \ldots N_{q}=M$ be the path from $N$ to $M$ through $T$.
By the definition of a cluster tree, it follows that $N_{i}$.label $<$
$N$.label, for $i > 1$ and therefore $\Delta(N_{i}) \ll \Delta(N)$. 
Thus
od($G[M],G[N]$) $\lleq$ (by the o.m.-triangle inequality)
$\max_{i=1 \ldots q-1}$(od($G[N_{i+1}],G[N_{i}]$)) $\lleq$ 
$\max_{i=1 \ldots q-1}$($\Delta(N_{i}$)) (since $N_{i+1}$ is the child
of $N_{i}$) $\lleq$ $\Delta(N)$.

\item[ii.] Let $N$ be a node in $T$; let $C_{1}$ and $C_{2}$ be two distinct
children of $N$; and let $M_{1}$ and $M_{2}$ be descendants of 
$C_{1}$ and $C_{2}$ respectively. Then od($G[M_{1}], G[M_{2}]$) = 
$\Delta(N)$. {\bf Proof:} By the construction of $x_{2} \ldots x_{p}$
in instantiate1($N$), od($G[C_{1}],G[C_{2}]$) = $\Delta(N)$.
By part (i.), od($G[M_{1}],G[C_{1}]$) $\lleq$ $\Delta(C_{1})$ $\ll$ $\Delta(N)$
and likewise
od($G[M_{2}],G[C_{2}]$) $\ll$ $\Delta(N)$.  Hence, by axiom A.6, 
od($G[M_{1}], G[M_{2}]$) = $\Delta(N)$.

\item[iii.] Let $a$ and $b$ be any two leaves in $T$, and let $N$
be the least common ancestor in $T$ of $a$ and $b$. Then od($G[a], G[b]$)
= $\Delta(N)$. {\bf Proof:} Immediate from (ii).

\item[iv.] For any node $N$, odiam($\Gamma$($N$)) = $\Delta(N)$. 
{\bf Proof:} From (iii), any two leaves descending from different children
of $N$ are at a distance of order $\Delta(N)$, and no two leaves of $N$
are at a distance of order greater than $\Delta(N)$. 

\item[v.] For any node $N$, $\Gamma$($N$) is a cluster of 
$\Gamma$($T$). {\bf Proof:} Let $a$ and $b$ be leaves of $N$, and
let $c$ be a leaf of $T - N$. Let $I$ be the common ancestor of $a$ and $b$
in $T$ and let $J$ be the common ancestor of $a$ and $c$.  Then
$I$ is either $N$ or a descendant of $N$ and $J$ is a proper ancestor of $N$.
Therefore by part (i), $\Delta(I) \ll \Delta(J)$. But by (iii), 
od($\Gamma(a), \Gamma(b)$) $=$ $\Delta(I)$ $\ll$ $\Delta(J)$ 
$=$ od($\Gamma(a),\Gamma(c)$).

\item[vi.] For any internal nodes $N,M$ if $M$.label $<$ $N$.label then 
odiam($\Gamma$($M$)) $\ll$ odiam($\Gamma$($N$)).
{\bf Proof:} Immediate from (iv) and the construction of $\Delta$.

\item[vii.] If $C$ is a cluster of $\Gamma(T)$ then 
there is a node $N$ in $T$ such that $C=\Gamma(N)$.  
{\bf Proof:} Let $S$ be the set of symbols corresponding to $C$ and let 
$N$ be the least common ancestor of all of $S$.  Let $a$
and $b$ be two symbols in $S$ that are in different subtrees of $N$.
Then by (iii), od($G[a], G[b]$) = $\Delta(N)$.  Let $x$ be any symbol in
$N$.symbols.  Then by (iii) od($G[a], G[x]$) $\lleq$ $\Delta(N)$. Hence
$G[x] \in C$.


% {\bf Proof of the
% contrapositive:} Let $S$ be any set of symbols that $\Gamma(S)$ is not
% a cluster.  Then there exists symbols $a,b \in S$, $c \not \in S$ such
% that od($\Gamma(a), \Gamma(b)$) is not much smaller than 
% od($\Gamma(a), \Gamma(c)$). Let $M$ be the least common ancestor in $T$ of
% $a$ and $b$, and let $N$ be the least common ancestor of $a$ and $c$. Then
% by part (i), $M$ is not a descendant of $N$.  Since $M$ and $N$ are
% both ancestors of $a$, $N$ must be a descendant of $M$. Therefore,
% % any node in $T$ whose leaves contain $a$ and $b$ must also contain $c$.
% Therefore, there is no node whose leaves are exactly $S$.

\end{itemize}

$\QED$
\subsection*{Proof of Theorem 1}
We here prove 
the correctness of algorithm solve\_constraints. We will 
assume throughout that the two variables in the long of any constraint
in $\cal S$ are distinct.


\vspace{.1in}
\noindent
{\bf Lemma 3:} 
Let $T$ be a cluster tree and let $\Gamma$ be an instantiation of $T$. 
Let $a$ and $b$ be symbols of $T$. Let $N$ be the least common ancestor
of $a$ and $b$ in $T$. Then od($\Gamma(a), \Gamma(b)$) =
odiam($\Gamma(N)$).

\vspace{.1in}
\noindent
{\bf Proof:} Since $\Gamma(a)$ and $\Gamma(b)$ are elements of 
$\Gamma$($N$), it follows from the definition of odiam that
od($\Gamma(a), \Gamma(b)$) $\lleq$ odiam($\Gamma(N)$). 
Suppose the inequality were strict; that is, 
od($\Gamma(a), \Gamma(b)$) $\ll$ odiam($\Gamma(N)$). 
Then let $C$ be the set of all the symbols $c$ of $T$
such that od($\Gamma(a),\Gamma(c)$) $\lleq$ od($\Gamma(a),\Gamma(b)$). 
Then odiam($\Gamma(C)$) = od($\Gamma(a),\Gamma(b)$) $\ll$ odiam($\Gamma(N)$).
It is easily shown that $\Gamma(C)$ is a cluster in
$\Gamma(T)$.  Therefore, by property (ii) of definition 5,
there must be a node $M$ such that $M$.symbols = $C$. Now, $M$ is certainly
not an ancestor of $N$, since odiam($\Gamma(M)$) $\ll$ odiam($\Gamma(N)$)
but $M$.symbols contains both $a$ and $b$. But this contradicts the
assumption that $N$ was the least common ancestor of $a$ and $b$.
$\QED$



\vspace{.1in}
\noindent
{\bf Corollary 4:} 
Let $T$ be a cluster tree and let $\Gamma$ be an instantiation of $T$. 
Let $a,b,c,d$ be symbols of $T$. 
Let $N$ be the least common ancestor of $c$ and $d$ in $T$, and
let $M$ be the least common ancestor of $a$ and $b$ in $T$. 
Then od($\Gamma(a), \Gamma(b)$) $\ll$ od($\Gamma(c), \Gamma(d)$) if and
only if $M$.label $<$ $N$.label.

\vspace{.1in}
\noindent
{\bf Proof:} Immediate from lemma 3 and property (iii) of definition
5 of instantiation. $\QED$

\vspace{.1in}
\noindent
{\bf Lemma 5:} Let $\cal S$ be any set of constraints of the form
od($a,b$) $\ll$ od($c,d$).  Let $H$ be the connected components of
the shorts of $\cal S$. If $\cal S$ is consistent, then not every
edge of $\cal S$ is in $H$.

\vspace{.1in}
\noindent
{\bf Proof:} Let $\Gamma$ be a valuation satisfying $\cal S$. Find
an edge $pq$ in $\cal S$ for which od($\Gamma(p),\Gamma(q)$) is maximal.
Now, if $ab$ is a short of $\cal S$ --- that is, there is a constraint
od($a,b$) $\ll$ od($c,d$) in $\cal S$ --- then od($\Gamma(a), \Gamma(b)$)
$\ll$ od($\Gamma(c), \Gamma(d)$) $\lleq$ od($\Gamma(p), \Gamma(q)$).

Now, let $ab$ be any edge in $H$, the connected components of the shorts of
$\cal S$. Then there is a path $a_{1}=a, a_{2} \ldots a_{k} =b$ such that
the edge $a_{i}a_{i+1}$ is a short of $\cal S$ for $i=1 \ldots k-1$. 
Thus, by the om-triangle inequality, 
od($\Gamma(a), \Gamma(b)$) $\lleq$ 
$\max_{i=1 .. k-1}(\mbox{od}(\Gamma(a_{i}), \Gamma(a_{i+1})))$ $\ll$
od($\Gamma(p), \Gamma(q)$). Hence $pq$ $\neq$ $ab$, so $pq$ is not in $H$.
$\QED$

\vspace{.1in}
\noindent
{\bf Lemma 6:} The values of $\cal S$ and $H$ in any iteration are supersets
of their values in any later iteration.

\vspace{.1in}
\noindent
{\bf Proof:} $\cal S$ is reset to a subset of itself at the end of each
iteration. $H$ is defined in terms of $\cal S$ in a monotonic manner. $\QED$

\vspace{.1in}
\noindent
{\bf Lemma 7:} 
$\cal S$ cannot be the same in two successive iterations of the main loop.

\vspace{.1in}
\noindent
{\bf Proof:} by contradiction. Suppose that $\cal S$ is the same in two
successive iterations. Then $H$ will be the same, since it is defined
in terms of $\cal S$. $H$ is constructed to contain all the shorts of $\cal S$,
Since the resetting of $\cal S$ at the end of the first iteration does
not change $\cal S$, $H$ must contain all the longs as well. Thus,
$H$ contains all the edges in $\cal S$. But that being the case, the
algorithm should have terminated with failure at the beginning of
the first iteration.  $\QED$


\vspace{.1in}
\noindent
{\bf Lemma 8:} 
Algorithm solve\_constraints always terminates.

\vspace{.1in}
\noindent
{\bf Proof:} By lemma 7, if the algorithm does not exit with failure, then
on each iteration some constraints are removed from $\cal S$. Hence, the
number of iterations of the main loop is at most the original size of 
$\cal S$. Everything else in the algorithm is clearly bounded. (Note
that this bound on the number of iterations is improved in Section 6.1
to $n-1$, where $n$ is the number of symbols.) 
$\QED$

 
\vspace{.1in}
\noindent
{\bf Lemma 9:} If algorithm solve\_constraints returns {\bf false}, then
$\cal S$ is inconsistent.

\vspace{.1in}
\noindent
{\bf Proof:} If the algorithm returns {\bf false}, then the transitive
closure of the shorts of $\cal S$ contains all the edges in $\cal S$.
By lemma 5, $\cal S$ is inconsistent.

\vspace{.1in}
\noindent
{\bf Lemma 10:}  If constraint $C$ of form od($a,b$) $\ll$ od($c,d$) is in the
initial value of $\cal S$, and edge $cd$ is in $H$ in 
some particular iteration, then constraint $C$ is in $\cal S$ at the
start of that iteration.

\vspace{.1in}
\noindent
{\bf Proof:} Suppose that $C$ is deleted from $S$ on some particular 
iteration. Then edge $cd$, the long of $C$, cannot be in 
$H$ in that iteration. That is, it is not possible for edge $cd$ to
persist in $H$ in an iteration after $C$ has been deleted from $\cal S$.
Note that, by lemma 6, once $cd$ is eliminated from $H$, it remains out
of $H$.
$\QED$

\vspace{.1in}
\noindent
{\bf Lemma 11:}  The following loop invariant holds: 
At the end of
each loop iteration, the values of $L$.symbols, where $L$ is a leaf in the 
current state of the tree, are exactly the connected components of $H$.

\vspace{.1in}
\noindent
{\bf Proof:} In the first iteration, $T$ is initially just the root $R$,
containing all the symbols, and a child of $R$ is created for each connected 
component of $H$.

Let $T_{i}$ and $H_{i}$ be the values of $T$ and $H$ at the end of the $i$th 
iteration.
Suppose that the invariant holds at the end of the $k$th iteration. 
By lemma 6, $H_{k+1}$ is a 
subset of $H_{k}$. Hence, each connected component of $H_{k+1}$ is a
subset of a connected component of $H_{k}$. Moreover, each connected component
$J$ of $H_{k}$ is either a connected component of $H_{k+1}$ or is partitioned
into several connected components of $H_{k+1}$. In the former case,
the leaf of $T_{k}$ corresponding to $J$ is unchanged and remains a leaf in
$T_{k+1}$. In the latter case, the leaf corresponding to $J$ gets assigned
one child for each connected component of $H_{k+1}$ that is a subset of $J$.
Thus, the connected components of $H_{k+1}$ correspond to the leaves of 
$T_{k+1}$.
$\QED$

\vspace{.1in}
\noindent
{\bf Lemma 12:}  If procedure solve\_constraints does not return {\bf false},
then it returns a well-formed cluster tree $T$.

\vspace{.1in}
\noindent
{\bf Proof:}
Using lemma 11, and the cleanup section of solve\_constraints which creates
the final leaves for symbols, it follows that every symbol in $\cal S$
ends up in a single leaf of $T$. As $m$ is decremented on each iteration,
and as no iteration adds both a new node and children of that node, it
follows that the label of each internal node is less than the label
of its father.  Hence the constraints on cluster trees (definition 3) are
satisfied. $\QED$

\vspace{.1in}
\noindent
{\bf Lemma 13:} 
Let $a,b$ be two distinct symbols in $\cal S$ and let $T$ be the cluster tree
returned by solve\_constraints for $\cal S$. Let $N$ be the least
common ancestor of $a,b$ in $T$. Then either $N$ is assigned its label
on the first iteration when the edge $ab$ is not in $H$, or the 
edge $ab$ is in the final value of $H$ when the loop is exited and 
$N$ is assigned its label in the final cleanup section.

\vspace{.1in}
\noindent
{\bf Proof:} As above, let $H_{i}$ be the value of $H$ in the $i$th 
iteration. 

If $N$ is the root, then it is assigned its label in the first
iteration. Clearly, $a$ and $b$, being in different subtrees of $N$,
must be in different connected components of $H_{1}$.

Suppose $N$ is assigned its label in the $k$th iteration of the loop for
$k>1$. 
By lemma 11, at the end of the previous iteration, 
$N$.symbols was a connected component of $H_{k-1}$, and it
therefore contained the edge $ab$.  Since $N$ is the least common ancestor
of $a,b$, it follows that $a$ and $b$ are placed in two different children
of $N$; hence, they are in two different connected components of $H_{k}$.
Thus the edge $ab$ cannot be in $H_{k}$.

Suppose $N$ is assigned its label in the cleanup section of the algorithm.
Then by lemma 11, $N$.symbols is a connected component of the final value
of $H$. Hence the
edge $ab$ was in the final value of $H$.
$\QED$

\vspace{.1in}
\noindent
{\bf Lemma 14:} 
Let $\cal S$ initially contain constraint $C$ of form 
od($a,b$) $\ll$ od($c,d$).
Suppose that solve\_constraints(${\cal S}$) returns a
cluster tree $T$. Let $M$ be the least common ancestor of $a,b$ in $T$ and 
let $N$ be the least common ancestor of $c,d$. Then $M$.label $<$ $N$.label.

\vspace{.1in}
\noindent
{\bf Proof:} Suppose $N$ is given a label in a given iteration. By
lemma 13, $cd$ is eliminated from $H$ in that same iteration. By lemma 10,
constraint $C$ must be in $\cal S$ at the start of the
iteration.  Hence $ab$ is a short of $S$ in the iteration, and 
is therefore in $H$. Hence
$M$ is not given a label until a later iteration, and therefore is
given a lower label.  

It is easily seen that $cd$ cannot be in $H$ in the final iteration of
the loop, and hence $N$ is not assigned its label in the cleanup
section. $\QED$

\vspace{.1in}
\noindent
{\bf Lemma 15:} 
Suppose that solve\_constraints(${\cal S}$) returns a 
cluster tree $T$. Then any instantiation of $T$ satisfies the constraints
$\cal S$.

\vspace{.1in}
\noindent
{\bf Proof:} Immediate from lemma 14 and corollary 4.

\vspace{.1in}
\noindent
{\bf Theorem 1:} 
The algorithm solve\_constraints(${\cal S}$) returns 
a cluster tree satisfying $\cal S$ if $\cal S$ is consistent, and returns 
{\bf false} if $\cal S$ is inconsistent.


\vspace{.1in}
\noindent
{\bf Proof:} If solve\_constraints($\cal S$) returns {\bf false}, then
it is inconsistent (lemma 9).  If it does not return {\bf false}, then
it returns a cluster tree $T$ (lemma 12). Since $T$ has an instantiation
(lemma 2) and since every instantiation of $T$ is a solution of $\cal S$
(lemma 15), it follows that $\cal S$ is consistent and $T$ satisfies $\cal S$.
$\QED$


\subsection*{Proof of Theorem 2}

\vspace{.1in}
\noindent
{\bf Lemma 16:} If ${\cal S}_{1}$ and ${\cal S}_{2}$
are consistent sets of constraints, and
${\cal S}_{1} \supset {\cal S}_{2}$ then \\
reduce\_constraints(${\cal S}_{1}$) $\supseteq$ 
reduce\_constraints(${\cal S}_{2}$).

\vspace{.1in}
\noindent
{\bf Proof:} Immediate by construction. The value of $H$ in the case
of ${\cal S}_{1}$ is a superset of its value in the case of ${\cal S}_{2}$,
and hence reduce\_constraints(${\cal S}_{1}$) is a superset of 
reduce\_constraints(${\cal S}_{2}$).

\vspace{.1in}
\noindent
{\bf Lemma 17:} If ${\cal S}_{1}$ and ${\cal S}_{2}$
are consistent sets of constraints, and
${\cal S}_{1} \supset {\cal S}_{2}$ then
num\_labels(${\cal S}_{1}$) $\geq$
num\_labels(${\cal S}_{2}$).

\vspace{.1in}
\noindent
{\bf Proof} by induction on num\_labels(${\cal S}_{2}$). If 
num\_labels(${\cal S}_{2}$) = 0, the statement is trivial. 
Suppose that the statement holds for all ${\cal S}^{\prime}$, where 
num\_labels(${\cal S}^{\prime}$) = $k$. \\
Let num\_labels(${\cal S}_{2}$) = $k+1$.  \\
Then $k+1$ = num\_labels(${\cal S}_{2}$) =
1 + num\_labels(reduce\_constraints(${\cal S}_{2}$)), so \\
$k$  =num\_labels(reduce\_constraints(${\cal S}_{2}$)). Now, suppose
${\cal S}_{1} \supset {\cal S}_{2}$. By lemma 16 \\
reduce\_constraints(${\cal S}_{1}$) $\supset$ 
reduce\_constraints(${\cal S}_{2}$). But then by the inductive
hypothesis \\
num\_labels(reduce\_constraints(${\cal S}_{1}$)) $\geq$
num\_labels(reduce\_constraints(${\cal S}_{2}$)), so \\
num\_labels(${\cal S}_{1}$) $\geq$
num\_labels(${\cal S}_{2}$). $\QED$

\vspace{.1in}
\noindent
{\bf Lemma 18:} Let $\cal S$ be a set of constraints, and let $\Gamma$ 
be a solution of $\cal S$.  For any graph $G$ over the symbols of 
$\cal S$, let nd($G,\Gamma$) be the number of different non-zero
values of od($a,b$) where edge $ab$ is in $G$.  Let edges($\cal S$)
be the set of edges in $\cal S$. Then nd(edges($\cal S$), $\Gamma$) $\geq$
num\_labels($\cal S$).

\vspace{.1in}
\noindent
{\bf Proof:} by induction on num\_labels($\cal S$).  If num\_labels($\cal S$)
= 0, then the statement is trivial.  Suppose for some $k$, the statement holds
for all ${\cal S}^{\prime}$ where num\_labels(${\cal S}^{\prime}$) = $k$,
and suppose num\_labels($\cal S$) = $k+1$.  Let $pq$ be the edge in 
$\cal S$ of maximal length.  For any set of edges $E$, let 
small-edges($E,\Gamma$) be the
set of all edges $ab$ in $E$ for which  \\
od($\Gamma(a), \Gamma(b)$) $\ll$ od($\Gamma(p), \Gamma(q)$). 
Since small-edges($E$) contains edges of every order of magnitude in $E$
except the order of magnitude of $pq$, it follows that \\
nd(small-edges($E,\Gamma$), $\Gamma$)
 = nd($E,\Gamma$) $-$ 1.  
Let $G$ be the complete graph over all the symbols in $\cal S$.
By the same argument as in lemma 5, small-edges($G,\Gamma$) $\supseteq$
$H$, where $H$ is the connected components of the shorts of $\cal S$, as
computed in reduce\_constraints($\cal S$).  Let ${\cal S}^{\prime}$ be 
the set of constraints
whose longs are in small-edges($G,\Gamma$). It follows that 
${\cal S}^{\prime}$ $\supseteq$ reduce\_constraints($\cal S$). \\
Now small-edges($G,\Gamma$)
$\supseteq$ edges(${\cal S}^{\prime}$) $\supseteq$ 
edges(reduce\_constraints($\cal S$)). \\
Hence 
nd(edges($\cal S$), $\Gamma$) = nd($G,\Gamma$) = 
nd(small-edges($G,\Gamma$), $\Gamma$) + 1 \\ $\geq$ 
nd(edges(reduce\_constraints($\cal S$))) + 1 $\geq$ 
(by the inductive hypothesis) \\
num\_labels(reduce\_constraints($\cal S$)) + 1  = num\_labels($\cal S$). $\QED$

\vspace{.1in}
\noindent
{\bf Theorem 2:} Out of all solutions to the set of constraints $\cal S$,
the instantiations of \\
solve\_constraints($\cal S$) have
the fewest number of different values of od($a,b$), where $a,b$
range over the symbols in $\cal S$. This number is given by 
num\_labels($\cal S$).

\vspace{.1in}
\noindent
{\bf Proof:} Immediate from lemma 18.

\vspace{.1in}
\noindent
{\bf Corollary 19:} Let $\Omega$ have all the properties of an om-space except
that it has only $k$ different orders of magnitude. A system of 
constraints $\cal S$ has a solution in $\Omega$ if and only if 
the tree returned by solve\_constraints($\cal S$) uses no more than
$k$ different labels.

\vspace{.1in}
\noindent
{\bf Proof:} Immediate from theorems 1 and 2. $\QED$

\subsection*{Proof of Algorithm for Non-strict Comparisons}

We now prove that the revised algorithm presented in Section 6.2 for non-strict
comparisons is correct.  The proof is only a slight extension of the proof
of theorem 1, given above. 
 
Recall that the revised algorithm in Section 6.2 replaces the line of
solve\_constraints

{\small
\begin{quote}
$H$ := the connected components of the shorts of $\cal S$ \\
\end{quote}
}
with the following code:

{\small
\begin{tabbing}
1. \hspace{1em} \=$H$ := the shorts of $\cal S$; \\
2. \> {\bf repeat} \=$H$ := the connected components of $H$; \\
3. \> \> {\bf for} \=each weak constraint od($a,b$) $\lleq$ od($c,d$)  \\
4. \> \> \>{\bf if} $cd$ is in $H$ then add $ab$ to $H$  
{\bf endif endfor} \\
5. \>{\bf until} no change has been made to $H$ in the last iteration.
\end{tabbing}
}

We need the following new lemmas and proofs:

\vspace{.1in}
\noindent
{\bf Lemma 20:} Let $\cal S$ be a set of strict comparisons, and let 
$\cal W$ be a set of non-strict comparisons. Let $H$ be the set of
edges output by the above code.
If ${\cal S } \cup \cal W$ is consistent, then there is an edge in $\cal S$
that is not in $H$.

\vspace{.1in}
\noindent
{\bf Proof:} As in the proof of lemma 5, let $\Gamma$ be a valuation 
satisfying ${\cal S} \cup \cal W$ and let $pq$ be an edge in $\cal S$
such that od($\Gamma(p), \Gamma(q)$) is maximal. We wish to show that,
for every edge $ab \in H$, od($\Gamma(a), \Gamma(b)$) $\ll$ 
od($\Gamma(p), \Gamma(q)$), and hence $ab \neq pq$. Proof by induction:
suppose that this holds for all the edges in $H$ at some point in the code,
and that $ab$ is now to be added to $H$. 
There are three cases to consider.

\begin{itemize}
\item $ab$ is added in step [1]. Then, as in lemma 5, there is a
constraint od($a,b$) $\ll$ od($c,d$) in $\cal S$. Hence
od($\Gamma(a), \Gamma(b)$)
$\ll$ od($\Gamma(c), \Gamma(d)$) $\lleq$ od($\Gamma(p), \Gamma(q)$).

\item $ab$ is added in step [2].
Then there is a path $a_{1}=a, a_{2} \ldots a_{k} =b$ such that
the edge $a_{i}a_{i+1}$ is in $H$ for $i=1 \ldots k-1$. 
By the inductive hypothesis, 
od($\Gamma(a_{i}),\Gamma(a_{i+1})$) $\ll$ od($\Gamma(p),\Gamma(q)$).
By the om-triangle inequality,  \\
od($\Gamma(a), \Gamma(b)$) $\lleq$ 
$\max_{i=1 .. k-1}(\mbox{od}(\Gamma(a_{i}), \Gamma(a_{i+1})))$ $\ll$
od($\Gamma(p), \Gamma(q)$). 

\item $ab$ is added in step [4].
Then there is a constraint od($a,b$) $\lleq$ od($c,d$) in $\cal W$ such
that $cd$ is in $H$. By the inductive hypothesis, od($\Gamma(c), \Gamma(d)$)
$\ll$ od($\Gamma(p), \Gamma(q)$).
\end{itemize}
$\QED$

\vspace{.1in}
\noindent
{\bf Lemma 21:} Let $\cal W$ contain the constraint od($a,b$) $\lleq$ od($c,d$).
Suppose that the algorithm returns a cluster tree $T$. Let $M$ be the
least common ancestor of $a$ and $b$ in $T$, and let $N$ be the least
common ancestor of $c$ and $d$. Then $M$.label $\leq$ $N$.label. 

\vspace{.1in}
\noindent
{\bf Proof:} By lemma 13, $N$ is assigned a label in the first iteration 
where $H$ does not include the edge $cd$. In all previous iterations, since
$cd$ is in $H$, $ab$ will likewise be put into $H$. Hence $M$ does not
get assigned a label before $N$, so $M$.label $\leq$ $N$.label.

The remainder of the proof of the correctness of the revised algorithm 
is exactly the same as the proof of theorem 1.

\subsection*{Validation of Algorithm  Solve\_constraints2}
The proof of the correctness of algorithm solve\_constraints2 is again
analogous in structure to the proof of theorem 1.  We sketch it below:
the details are not difficult to fill in.

\begin{itemize}
\item[1.] (Analogue of lemma 2:) If $T$ is an ordered cluster tree, then
the revised version of 
instantiate($T$) returns an instantiation of $T$.  The proof is exactly
the same as lemma 2, with the additional verification that instantiate2
preserves the orderings in $T$.

\item[2.] (Analogue of lemma 5:) Let $\cal S$ be a set of order-of-magnitude
constraints on distances, and let $\cal O$ be a set of ordering constraints
on points.  Let $H$ be the graph given by the two statements
\begin{quote}
$H$ := the connected components of the shorts of $\cal S$; \\
$H$ := incorporate\_order($H, \cal O$);      
\end{quote}
If $\cal S$ and $\cal O$ are consistent, then $H$ does not contain all 
the edges of $\cal S$.

{\bf Proof:} As in the proof of lemma 5, choose a valuation $\Gamma$ satisfying
$\cal S,O$ and let $pq$ be an edge in $\cal S$ for which od($\Gamma(p),
\Gamma(q)$) is maximal.  Following the informal argument presented in 
Section 6.3, it
is easily shown that $pq$ is longer than any of the edges added in
these two statements, and hence it is not in $H$.

\item[3.] (Analogue of lemma 9:) 
If solve\_constraints2 returns {\bf false}, then $\cal S,O$ is
inconsistent.  {\bf Proof:} Immediate from (2).

\item[4.] (Analogue of lemma 12:) If solve\_constraints2($\cal S,O$) does
not return false, then it returns a well-formed ordered cluster tree.

{\bf Proof:} 
By merging the strongly connected components of $G$, incorporate\_order
always ensures that the ordering arcs between connected components of $H$
form a DAG.  These arcs are precisely the same ones that are later added
among the children of node $N$ as ordering arcs.  Thus, 
the ordering arcs over the children of a node in the
cluster tree form a DAG. Otherwise, the construction of the tree $T$
is the same as in lemma 12.
\end{itemize}

The remainder of the proof is the same as the proof of theorem 1.

\subsection*{Proof of Theorem 3}

We begin by proving lemma 22, that the revised version of ``instantiate'',
given in Section 6.3, gives an instantiation of a cluster tree in 
Euclidean space.

\vspace{.1in}
\noindent
{\bf Lemma 22:} Any cluster tree $T$ has an instantiation in  Euclidean 
space $\Re^{m}$ of any dimensionality $m$.

The proof is essentially the same as
the proof of Lemma 2, except that we now have to keep track of
real quantities.  For any node $N$, if $i$=$N$.label, we define
$\Delta(N) = \delta_{i}$. The proof then proceeds in the following 
steps:

\begin{itemize}
\item[i.] For any $i< j$, $\delta_{i} < \delta_{j} / \alpha^{j-i}$.
Immediate by construction.

\item[ii.] For any nodes $M$,$C$, if $M$ is a descendant of $C$ in $T$ then \\
dist($G[M],G[C]$) $<$ $\alpha n \Delta(C) / (\alpha - 1)$.

{\bf Proof:} Let 
$C=C_{0}, C_{1} \ldots C_{r}=M$ be the path from $C$ to $M$ through $T$.
Then \\
\hspace*{2em} dist($G[M],G[C]$) $\leq$ (by the triangle inequality)
$\sum_{i=0}^{r-1}$dist($G[C_{i+1}],G[C_{i}]$) $\leq$  \\
\hspace*{2em} $\sum_{i=0}^{r-1}(n \Delta(C) / \alpha^{i})$ $<$
$(\alpha/(\alpha-1)) (n \Delta(C))$.

\item[iii.] Let $N$ be a node in $T$; let $C_{1}$ and $C_{2}$ be two
children of $N$; and let $M_{1}$ and $M_{2}$ be descendants of 
$C_{1}$ and $C_{2}$ respectively. Then  \\
\hspace*{2em} $\Delta(N) (1 - 2n/(\alpha-1))$ $<$ 
dist($G[M_{1}], G[M_{2}]$) $<$ 
$n\Delta(N) (1 + 2/(\alpha-1))$  \\
{\bf Proof:} By the triangle inequality, \\
\hspace*{2em} dist($G[C_{1}], G[C_{2}]$) $\leq$
dist($G[C_{1}],G[M_{1}]$) +
dist($G[M_{1}],G[M_{2}]$) +
dist($G[M_{2}],G[C_{2}]$). \\
Thus, 
dist($G[C_{1}], G[C_{2}]$) $-$
dist($G[C_{1}],G[M_{1}]$) $-$
dist($G[M_{2}],G[C_{2}]$) $\leq$
dist($G[M_{1}],G[M_{2}]$).  \\
Also, by the triangle inequality, \\
\hspace*{2em}
dist($G[M_{1}],G[M_{2}]$) $\leq$
dist($G[C_{1}], G[C_{2}]$) +
dist($G[C_{1}],G[M_{1}]$) +
dist($G[M_{2}],G[C_{2}]$). \\
By construction,  $\Delta(N)$ $\leq$ 
dist($G[C_{1}],G[C_{2}]$) $<$ $n \Delta(N)$, \\
and by part (ii), for $i = 1,2$,  
dist($G[M_{i}],G[C_{i}]$) $<$ $\alpha n \Delta(C) / (\alpha - 1)$ $<$
$n \Delta(N) / (\alpha -1)$ \\
as $\Delta(C) < \Delta(N) / \alpha$.

\item[iv.]
For any symbols $a,b,c,d$ in $T$, let $P$ be the least common ancestor of $a,b$
and let $N$ be the least common ancestor of $c,d$. If $P$.label $<$ $N$.label
then \\
much\_closer($G[a],G[b],G[c],G[d]$).

{\bf Proof:} By part (iii), dist($G[a],G[b]$) $<$ 
$n\Delta(P) (1 + 2/(\alpha-1))$ \\
and dist($G[c],G[d]$) $>$ $\Delta(N) (1 - 2n/(\alpha -1))$. Since
$\Delta(P) < \Delta(N) / \alpha$ and since \\
$\alpha = 2+2n+Bn$, it
follows by straightforward algebra that \\
dist($G[a],G[b]$) $<$ dist($G[c],G[d]$) / $B$.
\end{itemize}
$\QED$


We next prove the analogue of lemma 5.

\vspace{.1in}
\noindent
{\bf Lemma 23:} Let $\cal S$ be a set of constraints over $n$ variables
of the form \\
``dist($a,b$) $<$ dist($c,d$) / $B$'', where $B > n$. 
If $\cal S$ is consistent, then there is some edge in $\cal S$ which
is not in the connected components of the shorts of $\cal S$.

\vspace{.1in}
\noindent
{\bf Proof:} Let $\Gamma$ be a valuation satisfying $\cal S$. Let 
$pq$ be the edge in $\cal S$ for which dist($\Gamma(p),\Gamma(q)$) is maximal.
Now, if $ab$ is a short of $\cal S$ --- that is, there is a constraint
much\_closer($a,b,c,d$) in $\cal S$ --- then dist($\Gamma(a), \Gamma(b)$)
$<$ dist($\Gamma(c), \Gamma(d)$)/$B$  $\leq$ dist($\Gamma(p), \Gamma(q)$)/$B$.

Now, let $ab$ be any edge in $H$, the connected components of the shorts of
$\cal S$. Then there is a simple path $a_{1}=a, a_{2} \ldots a_{k} =b$ such that
the edge $a_{i}a_{i+1}$ is a short of $\cal S$ for $i=1 \ldots k-1$. 
Note that $k \leq n$.  Then, by the triangle inequality, 
\begin{quote}
dist($\Gamma(a), \Gamma(b)$) $\leq$ \\
dist($\Gamma(a_{1}),\Gamma(a_{2})$) + 
dist($\Gamma(a_{2}),\Gamma(a_{3})$) + \ldots +
dist($\Gamma(a_{k-1}),\Gamma(a_{k})$) $\leq$ \\
$(k-1)$dist($\Gamma(p), \Gamma(q)$) / $B$ $<$ dist($\Gamma(p), \Gamma(q)$) 
\end{quote}
Hence $pq$ $\neq$ $ab$, so $pq$ is not in $H$.
$\QED$

\vspace{.1in}
\noindent
{\bf Theorem 3:} Let $\cal S$ be a set of constraints over $n$ variables
of the form ``dist($a,b$) $<$ dist($c,d$) / $B$'', where $B > n$. 
The algorithm solve\_constraints(${\cal S}$) returns 
a cluster tree satisfying $\cal S$ if $\cal S$ is consistent over Euclidean 
space, and returns 
{\bf false} if $\cal S$ is inconsistent.

\vspace{.1in}
\noindent
{\bf Proof:}
Note that the semantics of the constraints ``much\_closer($a,b,c,d$)''
enters into the proof of Theorem 1 only in lemmas 2 and 5. The remainder
of the proof of Theorem 1 has to do purely with the relation between the
structure of $\cal S$ and the structure of the tree. Hence, since we have
shown that the analogues of lemmas 2 and 5 hold in a set of constraints
of this kind, the same proof can be completed in exactly the same way. 
$\QED$

\subsection*{Proof of Theorem 4}

\vspace{.1in}
\noindent
{\bf Lemma 24:} Let $T$ be a cluster tree and let $\Gamma$ be a valuation
over om-space $\Omega$ satisfying $T$. Let $x$ be a symbol not in $T$, 
let $a$ be a point in $\Omega$, and let $\Gamma^{\prime}$ be the valuation
$\Gamma \cup \{ x \rightarrow a \}$. Then there exists an extension 
$T^{\prime}$ of $T$ by $x$ such that $\Gamma^{\prime}$ satisfies $T^{\prime}$.

\vspace{.1in}
\noindent
{\bf Proof:} If $T$ is the empty tree, the statement is trivial. If
$T$ contains the single symbol $y$, then if $a = \Gamma(y)$ then 
operation (2) applies with $M$.label=0; if $a \neq \Gamma(y)$ then 
operation (2) applies with $M$.label=1.

Otherwise, let $y$ be the symbol in $T$ such that od($\Gamma(y),a$) is
minimal.  (We will deal with the case of ties in step (D) below.)
Let $F$ be the father of $y$ in $T$. 

Let $D$=od($\Gamma(y),a$). 
Let $V$ be the set of all orders of magnitude od($\Gamma(p), \Gamma(q)$), 
where $p$ and $q$ range over symbols in $T$. We define $L$ to be the 
{\em suitable label for $D$} as follows: If $D \in V$, then $L$ is the
label in $T$ corresponding to $D$. If $D$ is larger than any value
in $V$ then $L$ is the label of the root of $T$ plus 1. If $D \not \in V$,
but some value in $V$ is larger than $D$, then 
let $D_{1}$ be the largest value in $V$ less than $D$; 
let $D_{2}$ be the smallest value in $V$ greater than $D$; 
let $L_{1}$, $L_{2}$ be the labels in $T$ corresponding to $D_{1}$, $D_{2}$;
and let $L = (L_{1} + L_{2})/2$.

One of the following must hold:
\begin{itemize}
\item[A.] $\Gamma(y) = a$, and $F$.label=0. Then apply operation (3) with
$N=F$.
\item[B.] $\Gamma(y) = a$ and $F$.label $\neq$ 0. Then apply operation (4)
with $M$.label = 0.
\item[C.] $\Gamma(y) \neq a$, but od($\Gamma(y),a$) is less than
od($\Gamma(z),a$) for any other symbol $z \neq y$ in $T$. 
Apply operation (4) with $M$.label set to the suitable value for $D$ in $T$.
\item[D.] There is more than one value $y_{1} \ldots y_{k}$ for which
od($\Gamma(y_{i}),a$) = $D$.  It is easily shown  that in this case there
is an internal node $Q$ such that $y_{1} \ldots y_{k}$ is just the
set of symbols in the subtree of $Q$. There are three cases to consider:
\begin{itemize}
\item[D.i] $D$=odiam($\Gamma$($Q$.symbols)). Then apply operation (3) with
$N = Q$. 
\item[D.ii] $D$ $>$ odiam($\Gamma$($Q$.symbols)), and $Q$ is not the
root. Then apply operation (5) with $C = Q$. Set $M$.label to be the 
suitable value for $D$.
(It is easily shown that $D$ $<$ odiam($\Gamma$($N$.symbols)),
where $N$ is the father of $Q$.)
\item[D.iii] $D$ $>$ odiam($\Gamma$($Q$.symbols)), and $Q$ is the root.
Apply operation (6).
\end{itemize}
\end{itemize}
$\QED$

\vspace{.1in}
\noindent
{\bf Lemma 25:} Let $A = \{ a_{1} \ldots a_{k} \}$ be a finite set of
points whose diameter has order-of-magnitude $D$. Then there exists
a point $u$ such that, for $i = 1 \ldots k$, od($u,a_{i}$) = $D$.

\vspace{.1in}
\noindent
{\bf Proof:} Let $b_{1} = a_{1}$. By axiom A.8 there exists an 
infinite collection of points
$b_{2}, b_{3} \ldots$ such that od($b_{i},b_{j}$) = $D$ for $i \neq j$. Now,
for any value $a_{i}$ there can be at most one value $b_{j}$ such
that od($a_{i}, b_{j}$) $\ll$ $D$; if there were two such values
$b_{j1}$ and $b_{j2}$,
then by the om-triangle inequality, od($b_{j1},b_{j2}$)
$\ll$ $D$. Hence,  all but $k$ different values of $b_{j}$
are at least $D$ from any of the $a_{i}$. Let $u$ be any of these
values of $b_{j}$. Then since od($u,a_{1}$) = $D$  and od($a_{1},a_{i}$)
$\lleq$ $D$ for all $i$, it follows that od($u,a_{i}$) $\lleq$ $D$
for all $a_{i}$. Thus, since od($u,a_{i}$) $\lleq$ $D$ but 
not od($u,a_{i}$) $\ll$ $D$, it follows that od($u,a_{i}$) = $D$. $\QED$



\vspace{.1in}
\noindent
{\bf Lemma 26:} Let $T$ be a cluster tree; let $\Gamma$ be a valuation
over om-space $\Omega$ satisfying $T$; and let $T^{\prime}$ be an
extension of $T$ by $x$. If $\Omega$ is dense and unbounded above,
then there is a value $a$ such that the valuation $\Gamma \cup \{ x 
\rightarrow a \}$ satisfies $T^{\prime}$.


\vspace{.1in}
\noindent
{\bf Proof:} For operations (1) and (2)  the statement is trivial. 

Otherwise, let $L$ be an extending label of $T$. If $L = 0$, then set $D = 0$.
If $L$ is in $T$, then let $D$ be the order of magnitude corresponding to $L$
in $T$ under $\Gamma$.
If $L_{1} < L < L_{2}$ where $L_{1}$ and $L_{2}$ are labels of consecutive
values in $T$, then let $D_{1}$ and $D_{2}$ be the orders of magnitude
corresponding to $L_{1}$, $L_{2}$ in $T$ under $\Gamma$. Let $D$ be
chosen so that $D_{1} \ll D \ll D_{2}$. If $L$ is greater than any
label in the tree, then choose $D$ to be greater than the diameter of the
tree under $\Gamma$.

If $T^{\prime}$ is formed from $T$ by operation (3), then using lemma 25
let $a$ be a point such that od($a,\Gamma(y)$) = odiam($N$) for all
$y$ in $N$.symbols. 

If $T^{\prime}$ is formed from $T$ by operation (4), then let $a$ be a 
point such that od($a,\Gamma(y)$) = $D$.

If $T^{\prime}$ is formed from $T$ by operation (5), then let $a$ be a 
point such that od($a,\Gamma(y)$) = $D$ for all $y$ in $C$.symbols.
(Note that, since $M$.label $<$ $N$.label,  $D$ $<$ odiam($N$.symbols).)

If $T^{\prime}$ is formed from $T$ by operation (6), then let $a$ be a 
point such that od($a,\Gamma(y)$) = $D$ for all $y$ in $R$.symbols.

In each of these cases, it is straightforward to verify that
$\Gamma \cup \{ x \rightarrow a \}$ satisfies $T^{\prime}$. 
$\QED$

As we observed in Section 8 regarding lemma 28, 
the conditions on $\Omega$ in lemma 26
are necessary, and the statement is false otherwise. For example,
let $\Omega$ be the om-space described in example I, Section 3, of
polynomials over an infinitesimal $\delta$. Then $\Omega$ is not
unbounded above; there is a maximum order-of-magnitude $O(1)$. 
Let $T$ be the starting tree of Figure 3 (upper-left corner),
and let $T^{\prime}$ be the result of applying operation 6 (middle bottom).
Let $\Gamma$ be the valuation $\{ u \rightarrow \delta, v \rightarrow 2\delta,
w \rightarrow 1 \}$. Then $\Gamma$ satisfies $T$, but it cannot be extended 
to a valuation that satisfies $T^{\prime}$, as that would require $x$ to
be given a value such that od($v,w$) $\ll$ od($x,w$), and no such value
exists within $\Omega$.  The point of the lemma
is that, if $\Omega$ is required to be both dense and unbounded above,
then we cannot get ``stuck'' in this way.


\vspace{.1in}
\noindent
{\bf Lemma 27:} Let $T$ be a cluster tree. Let $X$ be a variable not among
 the symbols of $T$.  Let $\alpha$ be an open formula
in $\cal L$, whose free variables are the symbols of $T$ and the variable
$X$. Let $\phi$ be the formula $\te_{X} \alpha$.  Let $\Omega$ be an om-space
that is dense and unbounded above. Then
there exists an instantiation $\Gamma$ of $T$ in $\Omega$ that satisfies
$\phi$ if and only if there exists an extension $T^{\prime}$ of $T$
and an instantiation $\Gamma^{\prime}$ of $T^{\prime}$ that extends $\Gamma$ 
and satisfies $\alpha$.

\vspace{.1in}
\noindent
{\bf Proof:} Suppose that there exists an instantiation $\Gamma$ of $T$
that satisfies $\te_{X} \alpha$. Then, by definition, there is a point
$a$ in $\Omega$ such that $\Gamma$ satisfies $\alpha(X/a)$. That is,
the instantiation $\Gamma \cup \{ X \rightarrow a \}$ satisfies $\alpha$.
Let $\Gamma^{\prime} = \Gamma \cup \{ X \rightarrow a \}$. By 
lemma 24, the cluster tree $T^{\prime}$ corresponding to $\Gamma^{\prime}$
is an extension of $T$.

Conversely, suppose that there exists  an extension $T^{\prime}$ of
$T$ and an instantiation $\Gamma^{\prime}$ of $T^{\prime}$ satisfying 
$\alpha$. Let $\Gamma$ be the restriction of $\Gamma^{\prime}$ to the
symbols of $T$. Then clearly $\Gamma$ satisfies the formula 
$\te_{X} \alpha$.
$\QED$



\vspace{.1in}
\noindent
{\bf Lemma 28:} Let $T$ be a cluster tree. Let $\phi$ be an open formula
in $\cal L$, whose free variables are the symbols of $T$. 
Let $\Omega$ be an om-space
that is dense and unbounded above. 
If one instantiation $\Gamma$ of $T$ in $\Omega$ satisfies $\phi$ then every 
instantiation of $T$ in $\Omega$ satisfies $\phi$.

\vspace{.1in}
\noindent
{\bf Proof:} We can assume without loss of generality that
the only logical symbols in $\phi$ are $\neg$ (not), $\wedge$ (and),
$\te$ (exists), = (equals) and variables names, and that the only non-logical
symbol is the predicate ``much\_closer''. We now proceed using structural
induction on the form of $\phi$. Note that
an equivalent statement of the inductive hypothesis is, ``For any
formula $\psi$, either $\psi$ is true under every instantiation of $T$,
or $\psi$ is false under every instantiation of $T$.''

Base case: If $\phi$ is an atomic formula ``$X = Y$'' or 
``much\_closer($W,X,Y,Z$)'' then this follows immediately from corollary 4.

Let $\phi$ have the form $\neg \psi$. If $\phi$ is true under 
$\Gamma$, then $\psi$ is false under $\Gamma$. By the inductive hypothesis,
$\psi$ is false under every instantiation of $T$. Hence $\phi$ is
true under every instantiation of $T$.

Let $\phi$ have the form $\psi \wedge \theta$. If $\phi$ is true under
$\Gamma$ then both $\psi$ and $\theta$ are true under $\Gamma$. By
the inductive hypothesis, both $\psi$ and $\theta$ are true under
every instantiation of $T$. Hence $\phi$ is true under every instantiation
of $T$.

Let $\phi$ have the form $\te_{X} \alpha$. If $\phi$ is true under
$\Gamma$ then by lemma 27, there exists an extension $T^{\prime}$ of
$T$ and a instantiation $\Gamma^{\prime}$ of $T^{\prime}$ such that
$\alpha$ is true under $\Gamma^{\prime}$. By the inductive
hypothesis, $\alpha$ is true under every instantiation of $T^{\prime}$.
Now, if $\Delta^{\prime}$ is an instantiation of $T^{\prime}$ that
satisfies $\alpha$, and $\Delta$ is the restriction of $\Delta^{\prime}$
to the variables in $T$, then clearly $\Delta$ satisfies $\te_{X} \alpha$.
But by lemma 26, every instantiation $\Delta$ of $T$ can be extended to
an instantiation $\Delta^{\prime}$ of $T^{\prime}$. Therefore,
every instantiation of $T$ satisfies $\phi$.
$\QED$

\vspace{.1in}
\noindent
{\bf Theorem 4:} Let $T$ be a cluster tree. Let $\phi$ be an open formula
in $\cal L$, whose free variables are the symbols of $T$. 
Let $\Omega$ be an om-space
that is dense and unbounded above. Algorithm decide($T,\phi$) returns
{\bf true} if $T$ satisfies $\phi$ and {\bf false} otherwise.

\vspace{.1in}

\noindent
{\bf Proof:} Immediate from the proof of lemma 28. $\QED$

\section*{References}

Cormen, T.H.,  Leiserson, C.E., and  Rivest. R.L. (1990). {\em Introduction to
Algorithms.} Cambridge, MA: MIT Press 

\vspace{.1in}

\noindent
Davis, E. (1990). Order of Magnitude Reasoning in Qualitative
Differential Equations.
In D. Weld and J. de Kleer (Eds.) {\em Readings in Qualitative 
Reasoning about Physical Systems}. San Mateo, CA: Morgan Kaufmann.  422-434.


\vspace{.1in}
\noindent
Keisler, J. (1976).  {\em Foundations of Infinitesimal Calculus.} 
Boston, MA: Prindle, Webber, and Schmidt.


\vspace{.1in}
\noindent
Mavrovouniotis, M. and Stephanopoulos, G. (1990). ``Formal 
Order-of-Magnitude Reasoning in Process Engineering.''
In D. Weld and J. de Kleer (Eds.) {\em Readings in Qualitative 
Reasoning about Physical Systems}. San Mateo, CA: Morgan Kaufmann.  323-336.



\vspace{.1in}
\noindent
Raiman, O. (1990). ``Order of Magnitude Reasoning.''
In D. Weld and J. de Kleer (Eds.) {\em Readings in Qualitative 
Reasoning about Physical Systems}. San Mateo, CA: Morgan Kaufmann.  318-322.



\vspace{.1in}
\noindent
Robinson, A. (1965).  {\em Non-Standard Analysis}.  Amsterdam: North-Holland
Publishing Co.


\vspace{.1in}
\noindent
Weld, D. (1990). ``Exaggeration.''
In D. Weld and J. de Kleer (Eds.) {\em Readings in Qualitative 
Reasoning about Physical Systems}. San Mateo, CA: Morgan Kaufmann.  417-421.



\end{document}

