Publications

  1. A majorizing semantics for hyperarithmetic sentences, Zap. Nauchn. Semin. LOMI 68 (1977), 30-37; transl. J. Sov. Math. 15 (1981)
  2. An approach to constructivization of Cantor's theory of sets, Zap. Nauchn. Semin. LOMI 68 (1977), 38-49; transl. J. Sov. Math. 15 (1981)
  3. Constructive models for set theory with extensionality, The L.E.J. Brouwer Centenary Symposium, Sudies in Logic 110 (1982), North-Holland, 123-147
  4. On cut elimination in the presence of Peirce rule, Archiv für Math. Log. u. Grundl. forsch. 26 (1987), 147-164
  5. Proof-theoretical Analysis; Weak systems of functions and classes, Annals of Pure and Applied Logic (APAL) 38 (1988), 1-121
  6. Generalizations of the one-dimensional version of the Kruskal-Friedman theorems, Journ. of Symb. Log. 54 (1989), 100-121
  7. Systems of iterated projective ordinal notations, etc., Archive for Math. Log. 29 (1989), 29-46
  8. Generalizations of the Kruskal-Friedman theorems, Journ. of Symb. Log. 55 (1990), 157-181
  9. Quasi-Ordinals and proof theory, Habilitationsschrift, Universität Tübingen (1992)
  10. Quasi-Ordinals and proof theory, Proc. Conference on Graph Minors, Contemporary Mathematics 147, (1993), 485-494
  11. Strong well-quasi-ordering tree theorem, Preprint (1993), talk at Fourteenth British Combinatorial Conference (Keele, 1993)
  12. A modified sentence unprovable in PA, Journ. of Symb. Log. 59 (1994), 1154-1157
  13. 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).
  14. Strong normalization and realizability, Bull. of Symb. Log. 1 (1995), 109-110
  15. Computability in Lukasiewicz fuzzy logic, Preprint (1996), talk at Lukasiewicz in Dublin'96
  16. Reduction calculi for Post Logics, Logic at Work, Studies in Fuzziness and Soft Computing 24 (1999), Physica-Verlag, 187-203
  17. Variable compactness in 1-order logic, L. J. of IGPL 7 (1999), 327-357
  18. Combinatorial principles relevant to finite variable logic, Proc. RelMiCS 2000, Jules Desharnais (ed.), Universite Laval (2000), 95-111
  19. Proof systems in Relation Algebra, Relational Methods for Computer Science Applications, Studies in Fuzziness and Soft Computing 65 (2001), Physica-Verlag, 219-237
  20. Finite proof theory. Basic results, Archive for Math. Log. (to appear)
  21. 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.
  22. 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.
  23. 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.
  24. Toward combinatorial proof of P < NP. Basic approach, in: Logical Approaches to Computational Barriers, CiE 2006 Swansea, Report # CSR 7-2006, 119-128.
  25. (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)
  26. A note on Costa-Doria 'exotic formalizations', Arch. Math. Logic 49:813-821 (2010); DOI 10.1007/s00153-010-0203-x
  27. (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)
  28. (with A. Weiermann) Phase transitions in Proof Theory, DMTCS proc. AM: 343-358 (2010)
  29. (with A. Weiermann), Phase transitions of iterated Higman-style well-partial-ordering, Arch. Math. Logic (2011); DOI 10.1007/s00153-011-0258-3