Proof mining

From Wikipedia, the free encyclopedia

In mathematical logic, proof mining is a research program ^[1] that analyzes formalized proofs, especially in analysis, to obtain explicit bounds or rates of convergence from proofs that, when expressed in natural language, appear to be nonconstructive. This research has led to improved results in analysis obtained from the analysis of classical proofs.

[edit] References

1. ^ Ulrich Kohlenbach (2008). Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer Verlag, Berlin, 1--536. 

• Ulrich Kohlenbach and Paulo Oliva, "Proof Mining: A systematic way of analysing proofs in analysis", Proc. Steklov Inst. Math, 242:136-164, 2003

• Paulo Oliva, "Proof Mining in Subsystems of Analysis", BRICS PhD thesis citeseer