
The NP Search Problems of Frege and Extended
Frege Proofs, 

together with S.R.Buss.
24 pages, accepted. 

Deciding logics of linear Kripke frames with
scattered end pieces, 

together with N. Preining. 9 pages, accepted in Soft Computing 2016. 

Cobham Recursive Set Functions, 

together with S.R.Buss, S.D. Friedman, M Müller and N Thapen.
APAL 2016, 167(3): 335369 

Safe Recursive Set Functions, 

together with S.R.Buss and S.D. Friedman.
JSL 2015, 80(3): 730762. 

Separating intermediate predicate logics of wellfounded and dually
wellfounded structures by monadic sentences, 

together with N. Preining. 21 pages.
J Logic Computation (2015) 25(3): 527547. 

Parity Games and Propositional Proofs, 

together with P. Pudlák and N. Thapen.
30 pages. ACM TOCL 2014, 15(2), 17:117:30. 

Improved Witnessing and Local Improvement
Principles for SecondOrder Bounded Arithmetic, 

together with S.R.Buss.
35 pages. ACM TOCL 2014, 15(1), 2:12:35. 

Corrected Upper Bounds for FreeCut Elimination, 

together with S.R.Buss.
TCS 2011, 412(39): 54335445. 

Characterising Definable Search Problems
in Bounded Arithmetic via Proof Notations, 

together with S.R.Buss. In: Ways of Proof Theory,
ed. R. Schindler, Ontos Series
on Mathematical Logic, pp. 65134, 2010. 

On the computational complexity of cutreduction, 

together with K.T.Aehlig.
Ann.Pure.Appl.Logic 2010, 161: 711736. 

Polynomial Local Search
in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic, 

together with S.R.Buss. Journal of Mathematical Logic 2009,
9(1): 103138. 

Continuous Fraisse Conjecture, 

together with M. Goldstern and N. Preining. Order 2008, 25: 281298. 

Linear Kripke Frames and Gödel Logics, 

together with N. Preining. JSL 2007, 72(1): 2644. 

Generalised dynamic ordinals  universal measures
for implicit computational complexity, 

Logic Colloquium '02,
LNL, 27, Assoc. Symb. Logic, La Jolla, CA, 2006, pp. 48  74. 

Uniform proof complexity, 

Journal of Logic and Computation 2005, 15: 433446. 

Separation results for the size of constantdepth propositional proofs, 

Ann.Pure.Appl.Logic 2005, 136: 3055, together with S. Buss. 

An Unexpected Separation Result in Linearly Bounded Arithmetic, 

Math. Log. Quart. 2005, 51: 191200, together with J. Johannsen. 

Preservation theorems and restricted consistency statements
in bounded arithmetic, 

Ann.Pure.Appl.Logic 2004, 126: 255280 

Dynamic ordinal analysis, 

Arch. Math. Logic 2003, 42: 303334. 

Ordinal Notations and WellOrderings in Bounded Arithmetic, 

Ann.Pure.Appl.Logic 2003, 120: 197223, together with S. Buss and C. Pollett 

Notations for Exponentiation, 

TCS 2002, 288(1): 319. 

Proving consistency of equational theories in bounded arithmetic, 

JSL 2002, 67(1): 279296. 

A nonwellfounded primitive recursive tree,
provably wellfounded for cor.e. sets, 

Arch.Math.Logic 2002, 41(3): 251257. 

Exact bounds for lengths of reductions in typed $\lambda$calculus, 

JSL 2001, 66(3): 12771285. 

Analyzing Gödel's
T via expanded head reduction trees, 

Math.Log.Quat. 2000, 46(4): 517536, together with A. Weiermann. 

Characterizing the elementary recursive functions
by a fragment of Gödel's T., 

Arch.Math.Logic 2000, 39: 475491, together with A. Weiermann 

Applications of cutfree infinitary derivations
to generalized recursion theory, 

Ann.Pure.Appl.Logic 1998, 94: 719, together with W. Pohlers. 

A term rewriting characterization of the
polytime functions and related complexity classes, 

Arch. Math. Logic 1996, 36: 1130, together with A. Weiermann. 