Jump to content

Proof mining

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by BG19bot (talk | contribs) at 21:59, 29 March 2016 (References: Remove blank line(s) between list items per WP:LISTGAP to fix an accessibility issue for users of screen readers. Do WP:GENFIXES and cleanup if needed. Discuss this at Wikipedia talk:WikiProject Accessibility#LISTGAP). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

In proof theory, a branch of mathematical logic, proof mining (or unwinding) is a research program 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.[1] This research has led to improved results in analysis obtained from the analysis of classical proofs.

References

  1. ^ Ulrich Kohlenbach (2008). Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer Verlag, Berlin. pp. 1–536.
  • Ulrich Kohlenbach and Paulo Oliva, "Proof Mining: A systematic way of analysing proofs in mathematics", Proc. Steklov Inst. Math, 242:136–164, 2003
  • Paulo Oliva, "Proof Mining in Subsystems of Analysis", BRICS PhD thesis citeseer