Publications
- A majorizing semantics for hyperarithmetic sentences, Zap. Nauchn. Semin. LOMI 68 (1977), 30-37; transl. J. Sov. Math. 15 (1981)
- An approach to constructivization of Cantor's theory of sets, Zap. Nauchn. Semin. LOMI 68 (1977), 38-49; transl. J. Sov. Math. 15 (1981)
- Constructive models for set theory with extensionality, The L.E.J. Brouwer Centenary Symposium, Sudies in Logic 110 (1982), North-Holland, 123-147
- On cut elimination in the presence of Peirce rule, Archiv für Math. Log. u. Grundl. forsch. 26 (1987), 147-164
- Proof-theoretical Analysis; Weak systems of functions and classes, Annals of Pure and Applied Logic (APAL) 38 (1988), 1-121
- Generalizations of the one-dimensional version of the Kruskal-Friedman theorems, Journ. of Symb. Log. 54 (1989), 100-121
- Systems of iterated projective ordinal notations, etc., Archive for Math. Log. 29 (1989), 29-46
- Generalizations of the Kruskal-Friedman theorems, Journ. of Symb. Log. 55 (1990), 157-181
- Quasi-Ordinals and proof theory, Habilitationsschrift, Universität Tübingen (1992)
- Quasi-Ordinals and proof theory, Proc. Conference on Graph Minors, Contemporary Mathematics 147, (1993), 485-494
- Strong well-quasi-ordering tree theorem, Preprint (1993), talk at Fourteenth British Combinatorial Conference (Keele, 1993)
- A modified sentence unprovable in PA, Journ. of Symb. Log. 59 (1994), 1154-1157
- Cut free formalization of logic with finitely many variables, Part I, Proc. CSL'94, LN in Comp. Sci. 933 (1995), 135-150.
An Automatic Theorem Prover for Relation Algebras (ARA) has been implemented by Carsten Sinz. It is based on my Reduction Predicate Calculi for n-variable logic (RPC_n). - Strong normalization and realizability, Bull. of Symb. Log. 1 (1995), 109-110
- Computability in Lukasiewicz fuzzy logic, Preprint (1996), talk at Lukasiewicz in Dublin'96
- Reduction calculi for Post Logics, Logic at Work, Studies in Fuzziness and Soft Computing 24 (1999), Physica-Verlag, 187-203
- Variable compactness in 1-order logic, L. J. of IGPL 7 (1999), 327-357
- Combinatorial principles relevant to finite variable logic, Proc. RelMiCS 2000, Jules Desharnais (ed.), Universite Laval (2000), 95-111
- Proof systems in Relation Algebra, Relational Methods for Computer Science Applications, Studies in Fuzziness and Soft Computing 65 (2001), Physica-Verlag, 219-237
- Finite proof theory. Basic results, Archive for Math. Log. (to appear)
- Finite methods in 1-order formalisms, Proc. Days of Logic and Computability '99, Annals of Pure and Applied Logic (APAL) 113/1-3 (2002), 121-151.
- Proof theory and Post-Turing analysis, Proc. Proof Theory in Computer Science, Dagstuhl 2001, LN in Comp. Sci. 2183) (2001), 130-152. See also APPENDIX.
- Combinatorial principles in finite variable logic, in: J. Desharnais, M. Frappier, W. MacCaull (Eds.), Relational Methods in Computer Science, Methodos Proceedings, Vol. 1 (2002), 39-64.
- Toward combinatorial proof of P < NP. Basic approach, in: Logical Approaches to Computational Barriers, CiE 2006 Swansea, Report # CSR 7-2006, 119-128.
- (with E. H. Haeusler, V. G. da Costa) Proof compressions with circuit-structured substitutions, Journal of Mathematical Sciences, 158(5):645-658 (2009); Zapiski Nauchn. Sem. POMI, 358:77-99 (2008)
- A note on Costa-Doria 'exotic formalizations', Arch. Math. Logic 49:813-821 (2010); DOI 10.1007/s00153-010-0203-x
- (with E. H. Haeusler and L. C. Pereira) Propositional proof compressions and DNF logic, Logic Journal of IGPL, 19(1):62-86 (2011); doi:10.1093/jigpal/jzq003 (2010)
- (with A. Weiermann) Phase transitions in Proof Theory, DMTCS proc. AM: 343-358 (2010)
- (with A. Weiermann), Phase transitions of iterated Higman-style well-partial-ordering, Arch. Math. Logic (2011); DOI 10.1007/s00153-011-0258-3