Hans Koch, Alain Schenkel, and Peter Wittwer,
"Computer-assisted proofs in analysis and programming in logic", 
 SIAM Reviews, 1996 (to appear; the paper is stored 
in the mathematical physics archive, <ahref="
http://www.ma.utexas.edu/mp$\_$arc/mp$\_$arc$\_$home.html"</a>, paper 94-394). 
<P>

This paper explains interval methods in Banach spaces to
prove the existence of solutions for functional equations.
<P>

As a case study, the authors consider the Feigenbaum equation
$\varphi(x)=\lambda^{-1}\varphi(\varphi(\lambda x))$ that stems from
dynamical systems theory. A dynamical system with
discrete time is an operator $T:X\to X$ 
that describes how a state $x(t)\in X$ at a moment of time $t$ is
transformed into the state $x(t+1)=T(x(t))$ at the next moment of
time. For an arbitrary $n$, we have $x(t+n)=T^n(x(t))$. 
How can we describe the asymptotic
behavior of a generic 1-D dynamical system (i.e., of a dynamical system
in which a state space $X$ is a real line)? The very term "asymptotic
behavior" means that for all sufficiently large $n$, the transformations
$T^n$ are similar. In particular, for large $n$, 
the transformations $T^n(x)$ and $T^{2n}(x)=T^n(T^n(x))$ 
must be similar. By {\it similar}, we mean that these operations may
be mathematically different, but they are physically equivalent in the
following sense: if we appropriately change the unit in which we
measure $x$ (to a new one that is $\lambda$ times smaller for some
$\lambda>0$), i.e., if we use $x'=\lambda\cdot x$ instead of $x$, 
then the expression for $T^{2n}$ in the new units will be
almost identical to the expression for $T^{n}$ in the old ones (and
the larger the $n$, the closer this similarity will be). In other words,
if $y=T^n(x)$, then $y'\approx T^{2n}(x')$, where 
$y'=\lambda\cdot y$ and $x'=\lambda\cdot x$. In other words, $\lambda
T^n(x)\approx T^n(T^n(\lambda x))$. When $n\to\infty$, then for the
limit transformation $T^n\to\varphi$, we get the Feigenbaum equation $\lambda
\varphi(x)=\varphi(\varphi(\lambda x))$. 
<P>

The Feigenbaum equation was derived for 1-D systems, but it appears in
multi-dimensional systems as well. 
<P>

The existence of a solution to this equation is usually proved by
showing that this equation describes a fixed point of a contraction
mapping in Banach space (i.e., a mapping $m$ for which
$\|m(x)-m(y)\|\le\beta\|x-y\|$ for some $\beta<1$). 
To check that the corresponding mapping is a contraction, the authors
use "intervals" in Banach space, i.e., balls with a polynomial as a
center and a given radius. 
<P>

The proof itself is not new, but it is a good illustration of 
general interval techniques. 
<P>

The paper also proposes 
a solution to the problem of publishing such proofs in an
understandable way: to write a proof in Prolog, the language of
logic programming. Also, this paper gives
an introduction to Prolog, so that even a reader without previous
exposure to programming should be able to verify the correctness of
the proof.
<P>

In addition, this paper contains an exhaustive list of 
references to computer assisted proofs in analysis.
<P>

Edited from the author's 
abstract and an abstract by P. Wittwer.