Abstract:
We call proof mining the process of logically analyzing
proofs in mathematics with the aim of obtaining new information. In this
survey paper we discuss, by means of examples from mathematics, some of the
main techniques used in proof mining. We show that those techniques not only
apply to proofs based on classical logic, but also to proofs which involve
non-effective principles such as the attainment of the infimum of ![$f\in
C[0,1]$](Abs/img1.gif)
and the convergence for bounded monotone sequences of reals. We also
report on recent case studies in approximation theory and fixed point theory
where new results were obtained
and the convergence for bounded monotone sequences of reals. We also
report on recent case studies in approximation theory and fixed point theory
where new results were obtainedAvailable as PostScript, PDF, DVI.