Complexity of index sets and translating functions. - Alexander Leitsch (Fundam. Informaticae, 1980)

Fiducial intervals for the waiting time in batch and time-sharing systems. - Alexander Leitsch (Computing, 1982)

Fast Subsumption Algorithms. - Georg Gottlob; Alexander Leitsch (European Conference on Computer Algebra (2), 1985)

Eine Methode zur automatischen Problemreduktion. - Matthias Baaz; Alexander Leitsch (ÖGAI, 1985)

On the Efficiency of Subsumption Algorithms - Georg Gottlob; Alexander Leitsch (J. ACM, 1985)

Strong splitting rules in automated theorem proving. - Matthias Baaz; Alexander Leitsch (EUROCAL, 1987)

Deciding Horn Classes by Hyperresolution. - Alexander Leitsch (CSL, 1989)

On Different Concepts of Resolution. - Alexander Leitsch (Math. Log. Q., 1989)

A Strong Problem Reduction Method Based on Function Introduction. - Matthias Baaz; Alexander Leitsch (ISSAC, 1990)

Model Building by Resolution. - Christian G. Fermüller; Alexander Leitsch (CSL, 1992)

Complexity of Resolution Proofs and Function Introduction. - Matthias Baaz; Alexander Leitsch (Ann. Pure Appl. Log., 1992)

Resolution Methods for the Decision Problem - Christian G. Fermüller; Alexander Leitsch; Tanel Tammet; N. K. Zamov (Springer, 1993)

Deciding Clause Classes by Semantic Clash Resolution. - Alexander Leitsch (Fundam. Informaticae, 1993)

A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation - Matthias Baaz; Christian G. Fermüller; Alexander Leitsch (LICS, 1994)

On Skolemization and Proof Complexity. - Matthias Baaz; Alexander Leitsch (Fundam. Informaticae, 1994)

Incompleteness of a First-Order Gödel Logic and Some Temporal Logics of Programs. - Matthias Baaz; Alexander Leitsch; Richard Zach (CSL, 1995)

Fast Cut-Elimination by Projection. - Matthias Baaz; Alexander Leitsch (CSL, 1996)

Hyperresolution and Automated Model Building. - Christian G. Fermüller; Alexander Leitsch (J. Log. Comput., 1996)

Completeness of a First-Order Temporal Logic with Time-Gaps. - Matthias Baaz; Alexander Leitsch; Richard Zach (Theor. Comput. Sci., 1996)

The Resolution Calculus. - Alexander Leitsch (Springer, 1997)

Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction. - Alexander Leitsch (FTP (LNCS Selection), 1998)

Decision Procedures and Model Building in Equational Clause Logic. - Christian G. Fermüller; Alexander Leitsch (Log. J. IGPL, 1998)

System Description: CutRes 0.1: Cut Elimination by Resolution. - Matthias Baaz; Alexander Leitsch; Georg Moser (CADE, 1999)

Cut Normal Forms and Proof Complexity. - Matthias Baaz; Alexander Leitsch (Ann. Pure Appl. Log., 1999)

Cut-elimination and Redundancy-elimination by Resolution. - Matthias Baaz; Alexander Leitsch (J. Symb. Comput., 2000)

Normal Form Transformations. - Matthias Baaz; Uwe Egly; Alexander Leitsch (Handbook of Automated Reasoning, 2001)

Resolution Decision Procedures. - Christian G. Fermüller; Alexander Leitsch; Ullrich Hustadt; Tanel Tammet (Handbook of Automated Reasoning, 2001)

Comparing the Complexity of Cut-Elimination Methods. - Matthias Baaz; Alexander Leitsch (Proof Theory in Computer Science, 2001)

Cut-Elimination: Experiments with CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (LPAR, 2004)

CERES in Many-Valued Logics. - Matthias Baaz; Alexander Leitsch (LPAR, 2004)

Proof Transformations and Structural Invariance. - Stefan Hetzl; Alexander Leitsch (Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006)

Proof Transformation by CERES. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (MKM, 2006)

Event-Related Outputs of Computations in P Systems. - Matteo Cavaliere; Rudolf Freund; Alexander Leitsch; Gheorghe Paun (J. Autom. Lang. Comb., 2006)

Towards a clausal analysis of cut-elimination. - Matthias Baaz; Alexander Leitsch (J. Symb. Comput., 2006)

Herbrand Sequent Extraction. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (AISC/MKM/Calculemus, 2008)

Transforming and Analyzing Proofs in the CERES-System. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (LPAR Workshops, 2008)

How to Acknowledge Hypercomputation? - Alexander Leitsch; Günter Schachner; Karl Svozil (Complex Syst., 2008)

Towards an algorithmic construction of cut-elimination procedures. - Agata Ciabattoni; Alexander Leitsch (Math. Struct. Comput. Sci., 2008)

CERES: An analysis of Fürstenberg's proof of the infinity of primes. - Matthias Baaz; Stefan Hetzl; Alexander Leitsch; Clemens Richter; Hendrik Spohr (Theor. Comput. Sci., 2008)

A Clausal Approach to Proof Analysis in Second-Order Logic. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (LFCS, 2009)

System Description: The Proof Transformation System CERES. - Tsvetan Dunchev; Alexander Leitsch; Tomer Libal; Daniel Weller 001; Bruno Woltzenlogel Paleo (IJCAR, 2010)

CERES in higher-order logic. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001 (Ann. Pure Appl. Log., 2011)

A Resolution Calculus for Second-order Logic with Eager Unification. - Alexander Leitsch; Tomer Libal (PAAR@IJCAR, 2012)

Towards CERes in intuitionistic logic. - Alexander Leitsch; Giselle Reis; Bruno Woltzenlogel Paleo (CSL, 2012)

Towards Algorithmic Cut-Introduction. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001 (LPAR, 2012)

System Feature Description: Importing Refutations into the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (PxTP, 2012)

PROOFTOOL: a GUI for the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (UITP, 2012)

Cut-Elimination and Proof Schemata. - Cvetan Dunchev; Alexander Leitsch; Mikheil Rukhaia; Daniel Weller 001 (TbiLLC, 2013)

CERES for First-Order Schemata - Cvetan Dunchev; Alexander Leitsch; Mikheil Rukhaia; Daniel Weller 001 (CoRR, 2013)

Introducing Quantified Cuts in Logic with Equality. - Stefan Hetzl; Alexander Leitsch; Giselle Reis; Janos Tapolczai; Daniel Weller 001 (IJCAR, 2014)

Cut-Elimination: Syntax and Semantics. - Matthias Baaz; Alexander Leitsch (Stud Logica, 2014)

Algorithmic introduction of quantified cuts. - Stefan Hetzl; Alexander Leitsch; Giselle Reis; Daniel Weller 001 (Theor. Comput. Sci., 2014)

A Note on the Complexity of Classical and Intuitionistic Proofs. - Matthias Baaz; Alexander Leitsch; Giselle Reis (LICS, 2015)

Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]. - David M. Cerna; Alexander Leitsch (CoRR, 2015)

Schematic Cut Elimination and the Ordered Pigeonhole Principle. - David M. Cerna; Alexander Leitsch (IJCAR, 2016)

Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]. - David M. Cerna; Alexander Leitsch (CoRR, 2016)

The problem of Pi_2-cut-introduction. - Alexander Leitsch; Michael Peter Lettmann (CoRR, 2016)

Ceres in intuitionistic logic. - David M. Cerna; Alexander Leitsch; Giselle Reis; Simon Wolfsteiner (Ann. Pure Appl. Log., 2017)

On the Complexity of Translations from Classical to Intuitionistic Proofs. - Matthias Baaz; Alexander Leitsch (FLAP, 2017)

CERES for first-order schemata. - Alexander Leitsch; Nicolas Peltier; Daniel Weller 001 (J. Log. Comput., 2017)

A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. - Matthias Baaz; Alexander Leitsch; Anela Lolic (LFCS, 2018)

The problem of Π2-cut-introduction. - Alexander Leitsch; Michael Peter Lettmann (Theor. Comput. Sci., 2018)

On the Generation of Quantified Lemmas. - Gabriel Ebner; Stefan Hetzl; Alexander Leitsch; Giselle Reis; Daniel Weller 001 (J. Autom. Reason., 2019)

Extraction of Expansion Trees. - Alexander Leitsch; Anela Lolic (J. Autom. Reason., 2019)

On the Unification of Term Schemata. - David M. Cerna; Alexander Leitsch; Anela Lolic (UNIF, 2020)

An abstract form of the first epsilon theorem. - Matthias Baaz; Alexander Leitsch; Anela Lolic (J. Log. Comput., 2020)

Schematic Refutations of Formula Schemata. - David M. Cerna; Alexander Leitsch; Anela Lolic (J. Autom. Reason., 2021)

Herbrand's Theorem in Inductive Proofs. - Alexander Leitsch; Anela Lolic (LPAR, 2024)

On Proof Schemata and Primitive Recursive Arithmetic. - Alexander Leitsch; Anela Lolic; Stella Mahler (LPAR Complementary Volume, 2024)

Towards an Analysis of Proofs in Arithmetic. - Alexander Leitsch; Anela Lolic; Stella Mahler (CoRR, 2025)