| 2024 | LPAR | Herbrand's Theorem in Inductive Proofs. | Alexander Leitsch, Anela Lolic |
| 2024 | LPAR | On Proof Schemata and Primitive Recursive Arithmetic. | Alexander Leitsch, Anela Lolic, Stella Mahler |
| 2018 | LFCS | A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. | Matthias Baaz, Alexander Leitsch, Anela Lolic |
| 2016 | CADE | Schematic Cut Elimination and the Ordered Pigeonhole Principle. | David M. Cerna, Alexander Leitsch |
| 2015 | LICS | A Note on the Complexity of Classical and Intuitionistic Proofs. | Matthias Baaz, Alexander Leitsch, Giselle Reis |
| 2014 | CADE | Introducing Quantified Cuts in Logic with Equality. | Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller |
| 2012 | CADE | A Resolution Calculus for Second-order Logic with Eager Unification. | Alexander Leitsch, Tomer Libal |
| 2012 | CSL | Towards CERes in intuitionistic logic. | Alexander Leitsch, Giselle Reis, Bruno Woltzenlogel Paleo |
| 2012 | LPAR | Towards Algorithmic Cut-Introduction. | Stefan Hetzl, Alexander Leitsch, Daniel Weller |
| 2010 | CADE | System Description: The Proof Transformation System CERES. | Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo |
| 2009 | LFCS | A Clausal Approach to Proof Analysis in Second-Order Logic. | Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo |
| 2008 | AISC | Herbrand Sequent Extraction. | Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo |
| 2008 | LPAR | Transforming and Analyzing Proofs in the CERES-System. | Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo |
| 2004 | LPAR | Cut-Elimination: Experiments with CERES. | Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr |
| 2004 | LPAR | CERES in Many-Valued Logics. | Matthias Baaz, Alexander Leitsch |
| 1999 | CADE | System Description: CutRes 0.1: Cut Elimination by Resolution. | Matthias Baaz, Alexander Leitsch, Georg Moser |
| 1996 | CSL | Fast Cut-Elimination by Projection. | Matthias Baaz, Alexander Leitsch |
| 1995 | CSL | Incompleteness of a First-Order Gdel Logic and Some Temporal Logics of Programs. | Matthias Baaz, Alexander Leitsch, Richard Zach |
| 1994 | LICS | A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation | Matthias Baaz, Christian G. Fermller, Alexander Leitsch |
| 1992 | CSL | Model Building by Resolution. | Christian G. Fermller, Alexander Leitsch |
| 1990 | ISSAC | A Strong Problem Reduction Method Based on Function Introduction. | Matthias Baaz, Alexander Leitsch |
| 1989 | CSL | Deciding Horn Classes by Hyperresolution. | Alexander Leitsch |