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)

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)

On the elimination of quantifier-free cuts. - Daniel Weller 001 (Theor. Comput. Sci., 2011)

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)

On the complexity of proof deskolemization. - Matthias Baaz; Stefan Hetzl; Daniel Weller 001 (J. Symb. Log., 2012)

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

Expansion Trees with Cut. - Stefan Hetzl; Daniel Weller 001 (CoRR, 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)

Exposition: Synthesis via Functional Interpretation. - Daniel Weller 001 (CoRR, 2014)

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

Preface. - Matthias Baaz; Agata Ciabattoni; Dov M. Gabbay; Stefan Hetzl; Daniel Weller 001 (J. Log. Comput., 2017)

Boolean unification with predicates. - Sebastian Eberhard; Stefan Hetzl; Daniel Weller 001 (J. Log. Comput., 2017)

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

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

Expansion trees with cut. - Federico Aschieri; Stefan Hetzl; Daniel Weller 001 (Math. Struct. Comput. Sci., 2019)