 94394 Hans Koch, Alain Schenkel, Peter Wittwer
 ComputerAssisted Proofs in Analysis and Programming in Logic: A Case Study
(171K, plain TeX)
Dec 16, 94

Abstract ,
Paper (src),
View paper
(auto. generated ps),
Index
of related papers

Abstract. In this paper we present a computerassisted proof
of the existence of a solution for the Feigenbaum equation
phi(x)=phi(phi(lambda*x))/lambda.
There exist by now various such proofs in the literature.
Although the one presented here is new, the main purpose of this paper
is not to provide yet another version,
but to give an easytoread and self contained introduction
to the technique of computerassisted proofs in analysis.
Our proof is written in Prolog (Programming in logic),
a programming language which we found to be well suited for this purpose.
In this paper we also give an introduction to Prolog,
so that even a reader without prior exposure to programming
should be able to verify the correctness of the proof.
 Files:
94394.tex