Since 2014
Proof Theory and Computational Analysis
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Proof Theory and Computational Analysis
|
|
| Creator |
Kohlenbach, Ulrich
|
|
| Description |
In this survey paper we start with a discussion how functionals of finite type can be used for the proof-theoretic extraction of numerical data (e.g. effectiveuniform bounds and rates of convergence) from non-constructive proofs in numerical analysis. We focus on the case where the extractability of polynomial bounds is guaranteed.This leads to the concept of hereditarily polynomial bounded analysis (PBA). We indicate the mathematical range of PBA which turns out to be surprisingly large. Finally we discuss the relationship between PBA and so-called feasible analysisFA. It turns out that both frameworks are incomparable. We argue in favor of the thesis that PBA offers the more useful approach for the purpose of extracting mathematically interesting bounds from proofs. In a sequel of appendices to this paper we indicate the expressive power of PBA.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1997-01-30
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18956
10.7146/brics.v4i30.18956 |
|
| Source |
BRICS Report Series; No 30 (1997): RS-30 Proof Theory and Computational Analysis
BRICS Report Series; Nr. 30 (1997): RS-30 Proof Theory and Computational Analysis 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18956/16595
|
|