Prof Stan S. Wainer 

Proof Theory and ComputationTopics: infinitary proof theory and ordinal analysis, proof transformations, subrecursive complexity, computability.There is a fundamental question which, since the pioneering contributions of Gödel, Gentzen and Herbrand seventy years ago, has motivated the continued development of that area of Mathematical Logic known as "Proof Theory", and which now drives much presentday activity at the LogicComputer Science interface, namely "What is the information content of a (constructive) formal proof and how can it be read off ?" If, from a formal proof of the specification, it were possible effectively to extract or synthesize a program P which satisfies it, then the program would automatically be a "verified" one. If, in addition, it were possible to read off from the proof, bounds on the existential theorems occurring in it, this would provide an effective way of estimating the complexity of P. If this connection between proofs and programs were sufficiently close, then "natural" transformations on proofs would correspond to natural program transformations. Mathematical logic provides theoretical and practical realizations of these possibilities. Subrecursive hierarchy classifications attempt to structure the computable functions by means of transfinite hierarchies which precisely reflect both their computational complexity and the logical complexity of their 'termination proofs'. Although no natural way has been found of classifying all computable functions in one hierarchy, prooftreoretically significant subclasses can be successfully analysed in terms of the socalled Fast and Slow growing hierarchies developed by Schwichtenberg, Wainer, Weiermann and others. This work has deep connections with various other branches of mathematical logic and computer science  Proof Theory, Independence Results, Finitary Combinatorics, Program Verification, Complexity Theory etc.

[ University of Leeds ] [ Mathematics ] [ Pure Maths ] [ Applied Maths ] [ Statistics ] This page is maintained by the Pure Mathematics Webmaster Last updated 13 October 2005 