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).
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
(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