2022W

• Bachelor Thesis for Informatics and Business Informatics / 185.A26 / PR
• Seminar in Logic / 192.132 / SE

• Algorithmic Structuring and Compression of Proofs
  2013 – 2016 / Austrian Science Fund (FWF)
• Proof Transformations via Cut-Elimination in Intuitionistic Logic
  2012 – 2015 / Austrian Science Fund (FWF)
• About Schemata and Proofs
  2010 – 2012 / Austrian Science Fund (FWF)
• Proof Theoretic Applications of CERES
  2010 – 2012 / Austrian Science Fund (FWF)
• Computer-aided analysis of inductive and second-order proofs
  2007 – 2009 / Austrian Science Fund (FWF)
• Automated Analysis of Mathematical Proofs
  2005 – 2007 / Austrian Science Fund (FWF)

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.

2021

• An abstract form of the first epsilon theorem / M. Baaz, A. Leitsch, A. Lolic / Journal of Logic and Computation, 30 (2021), 8; 1447 - 1468
• Schematic Refutations of Formula Schemata / A. Leitsch, D. Cerna, A. Lolic / Journal of Automated Reasoning, 65 (2021), 5; 599 - 645

2020

• Schematic Refutations of Formula Schemata / D. Cerna, A. Leitsch, A. Lolic / Journal of Automated Reasoning, online (2020)

2019

• Extraction of Expansion Trees / A. Lolic, A. Leitsch / Journal of Automated Reasoning, 62 (2019), 3; 393 - 430
• On the Generation of Quantified Lemmas / G. Ebner, S. Hetzl, A. Leitsch, G. Reis, D. Weller / Journal of Automated Reasoning, 63 (2019), 1; 95 - 126
• Schematic Refutations of Formula Schemata / D. Cerna, A. Leitsch, A. Lolic / ArXiv, 1902.08055 (2019), 52 pages

2018

• A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem / A. Leitsch, M. Baaz, A. Lolic / Keynote Lecture: Logical Foundations of Computer Science - International Symposium, LFCS 2018, Florida (invited); 2018-01-08 - 2018-01-11; in: "LNCS 10703", Springer International Publishing AG, 10703 (2018), 55 - 71
• Extraction of Expansion Trees / A. Lolic, A. Leitsch / Journal of Automated Reasoning, 61 (2018), 1; 1 - 38

2017

• Expansion Trees from Non-Normalized Proofs with CERES / A. Lolic, A. Leitsch / Talk: Collegium Logicum Proof Theory: Herbrand's Theorem Revisited, Wien; 2017-05-25 - 2017-05-27
• The problem of Pi_2-cut-introduction / A. Leitsch, M. Lettmann / Theoretical Computer Science, 706 (2017), 83 - 116
• {CERES} for first-order schemata / A. Leitsch, D. Weller et al. / Journal of Logic and Computation, 27 (2017), 7; 1897 - 1954
• Ceres in intuitionistic logic / A. Leitsch, D. Cerna, G. Reis et al. / Annals of Pure and Applied Logic, 168 (2017), 10; 1783 - 1836

2016

• CERES in intuitionistic logic completeness / A. Leitsch / Talk: Magica 16, Mailand (invited); 2016-09-26 - 2016-09-27
• Schematic Cut Elimination and the Ordered Pigeonhole Principle / A. Leitsch, D. Cerna / Talk: IJCAR 2016, Coimbra; 2016-06-27 - 2016-07-02; in: "Automated Reasoning - 8th International Joint Conference, {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings", N. Olivetti et al. (ed.); 9706 (2016), ISBN: 978-3-319-40229-1; 241 - 256
• Schematic Cut elimination and the Ordered Pigeonhole Principle / A. Leitsch, D. Cerna / CoRR - Computing Research Repository, abs/1601.06548 (2016), abs/1601.06548

2015

• A Note on the Complexity of Classical and Intuitionistic Proofs / A. Leitsch, M. Baaz, G. Reis / Talk: Thirtieth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS), Kyoto; 2015-07-06 - 2015-07-10; in: "Logic in Computer Science (LICS)", (2015), ISSN: 1043-6871; 657 - 666
• On Proof Mining by Cut-Elimination / A. Leitsch et al. / in: "All about Proofs, Proofs for All", 55; B. Woltzenlogel-Paleo et al. (ed.); College Publications, 2015, ISBN: 978-1-84890-166-7, 173 - 200
• Analysis of Clause set Schema Aided by Automated Theorem Proving: {A} Case Study [Extended Paper] / A. Leitsch, D. Cerna / Computing Research Repository (CoRR), abs/1503.08551 (2015), 15 pages

2014

• Mathematical Proof Analysis / A. Leitsch / Keynote Lecture: VSL 2014, Wien; 2014-07-12 - 2014-07-26
• Cut-Elimination: Syntax and Semantics / M. Baaz, A. Leitsch / Studia Logica, 102 (2014), 6; 1217 - 1244
• Algorithmic introduction of quantified cuts / S. Hetzl, A. Leitsch, G. Reis, D. Weller / Theoretical Computer Science, 549 (2014), 1 - 16
• Introducing Quantified Cuts in Logic with Equality / S. Hetzl, A. Leitsch, G. Reis, J. Tapolczai, D. Weller / in: "Automated Reasoning - 7th International Joint Conference", issued by: IJCAR; LNCS 8562, Springer, 2014, 240 - 254
• Introducing Quantified Cuts in Logic with Equality / A. Leitsch, S. Hetzl, G. Reis, D. Weller et al. / CoRR - Computing Research Repository, abs/1402.2474 (2014), abs/1402.2474; 16 pages

2013

• Methods of Cut-Elimination / A. Leitsch / Talk: Ninth International Tbilisi Summer School in Logic and Language, Tbilisi, Georgia; 2013-09-30 - 2013-10-04
• Prooftool: a GUI for the GAPT Framework / A. Leitsch, T. Libal, M. Riener, D. Weller, B. Woltzenlogel-Paleo, T. Dunchev / Talk: 10th International Workshop On User Interfaces for Theorem Provers, Bremen; 2013-07-11; in: "Proceedings 10th International Workshop on User Interfaces for Thorem Provers,", C. Kaliszyk et al. (ed.); (2013), ISSN: 2075-2180; 1 - 14
• A method of algorithmic cut-introduction / A. Leitsch / Talk: Workshop on Skolemization, Utrecht; 2013-05-27 - 2013-05-29
• Ceres for First-Order Schemata / A. Leitsch, T. Dunchev, D. Weller, M. Rukhaia / CoRR - Computing Research Repository, arXiv:1303.4257 (2013), 1 - 40

2012

• CERES for First-Order Schemata / A. Leitsch / Talk: Collegium Logicum 2012: Structural Proof Theory, Paris, France; 2012-11-15 - 2012-11-16
• System feature description: importing refutations into the GAPT framework / C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel-Paleo / Talk: Proof Exchange for Theorem Proving, Second International Workshop, Manchester, UK; 2012-06-30; in: "Proceeding of Proof Exchange for Theorem Proving | Second International Workshop, PxTP 2012", D. Pichardie, T. Weber (ed.); (2012), ISSN: 1613-0073; 51 - 57
• Towards Algorithmic Cut-Introduction / A. Leitsch, S. Hetzl, D. Weller / in: "Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18", N. Bjorner, A. Voronkov (ed.); Springer LNCS, 2012, ISBN: 978-3-642-28716-9, 228 - 242
• Towards CERes in intuitionistic logic / A. Leitsch, G. Reis, B. Woltzenlogel-Paleo / in: "Computer Science Logic (CSL'12) - 26th International Workshop/21st", P. Cegielski et al. (ed.); Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2012, ISBN: 978-3-939897-42-2, 485 - 499

2011

• Towards algorithmic cut-introduction / A. Leitsch / Talk: 2nd Workshop of the Joint Project "Structural and Computational Proof Theory", Innsbruck; 2011-10-26 - 2011-10-28
• Methods of cut-elimination / M. Baaz, A. Leitsch / Springer Verlag, 2011, ISBN: 978-94-007-0319-3; 287 pages
• Ceres in higher-order logic / S. Hetzl, A. Leitsch, D. Weller / Annals of Pure and Applied Logic, 162 (2011), 12; 1001 - 1034

2010

• CERES in higher-order-logic / A. Leitsch / Talk: Collegium Locicum 2010: Proofs and Structures, Paris (invited); 2010-11-08 - 2010-11-10
• CERES in higher-order-logic / S. Hetzl, A. Leitsch, D. Weller / Talk: Workshop on Classical Logic and Computation (CL&C'10), Brünn; 2010-08-22
• Fast Cut-Elimination by CERES / A. Leitsch, M. Baaz / in: "Proofs, Categories and Computations", S. Feferman, W. Sieg (ed.); College Publications, London, 2010, ISBN: 978-1-84890-012-7, 31 - 49
• Fast cut-elimination by CERES / M. Baaz, A. Leitsch / in: "Proofs, Categories and Computations, Essays in Honor of Grigori Mints", S. Feferman, W. Sieg (ed.); College Publications (Kings College), 2010, ISBN: 978-1-84890-012-7, 31 - 48
• System Description: The Proof Transformation System CERES / A. Leitsch, T. Dunchev, D. Weller, B. Woltzenlogel-Paleo, T. Libal / in: "IJCAR 2010", J. Giesl, R. Hähnle (ed.); Springer, LNAI, Heidelberg, 2010, ISBN: 978-3-642-14202-4, 427 - 433

2009

• Fast Cut-Elimination by CERES / A. Leitsch / Talk: Moscow-Vienna Workshop on Logic and Computation 2009, Wien (invited); 2009-06-29 - 2009-07-02
• A Clausal Approach to Proof Analysis in Second-Order Logic / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / Talk: Symposium on Logical Foundations of Computer Science (LFCS 2009), Deerfield Beach, FL, USA; 2009-01-03 - 2009-01-06; in: "Logical Foundations of Computer Science", A. Nerode, S. Artemov (ed.); Springer, LNCS, 5407 (2009), ISBN: 3-540-92686-0; 214 - 229
• A Clausal Approach to Proof Analysis in Second-Order Logic / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / in: "Lecture Notes in Computer Science, 5407", E. Artemov, A. Nerode (ed.); Springer LNCS, Heidelberg, 2009, ISBN: 3-540-92686-0, 214 - 229

2008

• Transforming and Analyzing Proofs in the CERES-system / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / Talk: The LPAR 2008 Workshops: KEAPPA and IWIL 2008, Doha, Qatar; 2008-11-22; in: "Proceedings of the LPAR 2008 Workshops", P. Rudnicki, G. Sutcliffe et al. (ed.); CEUR-WS.org, Vol 418 (2008), ISSN: 1613-0073; 77 - 91
• CERES: Analysis of the fifth Proof of the Infinity of Primes / A. Leitsch / Talk: Non-classical Logics: from Foundations to Applications, Pisa (invited); 2008-04-24 - 2008-04-26
• How to Acknowledge Hypercomputation / A. Leitsch, G. Schachner, K. Svozil / Complex Systems, 18 (2008), 131 - 143
• CERES: An analysis of Fürstenberg's proof of the infinity of primes / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Theoretical Computer Science, 403 (2008), 2-3; 160 - 175
• Towards an algorithmic construction of cut-elimination procedures / A. Ciabattoni, A. Leitsch / Mathematical Structures In Computer Science, 18 (2008), 1; 81 - 105
• Herbrand Sequent Extraction / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / in: "AISC/Calculemus/MKM 2008", S. Autexier et al. (ed.); Springer, Heidelberg, 2008, ISBN: 9783540851097, 462 - 477
• Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions / A. Leitsch, S. Hetzl, D. Weller, B. Woltzenlogel-Paleo / in: "Proceedings of the CICIM Workshops on ESARM-08", G. Sutcliffe, S. Colton, S. Schulz (ed.); issued by: Ceur Workshop Proceedings; CEUR-WS.org, 2008, ISSN: 1613-0073, 23 - 41

2007

• CERES: An analysis of Fürstenberg's proof of the infinity of primes / A. Leitsch / Keynote Lecture: Moscow-Vienna Workshop on Logic and Computation, Wien; 2007-07-02 - 2007-07-03
• Proof Transformations and Structural Invariance / A. Leitsch, S. Hetzl / in: "LNAI 4460: Algebraic and Proof-theoretic Aspects", S. Aguzzoli et al. (ed.); Springer, LNAI 4460, 2007, 201 - 230

2006

• System Description: The Cut-Elimination System CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Talk: FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR), Seattle, USA; 2006-08-21; in: "ESCoR 2006 Empirically Successful Computerized Reasoning", G. Sutcliffe, R. Schmidt, S. Schulz (ed.); CEUR Workshop Proceedings, 192 (2006), ISSN: 1613-0073; Paper ID 11, 9 pages
• CERES: Cut-Elimination by Resolution / A. Leitsch / Talk: MANYVAL 06, Gargnano; 2006-03-20 - 2006-03-22
• Proof transformation by CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Lecture Notes in Computer Science, 4108 (2006), 82 - 93
• Towards a clausal analysis of cut-elimination / M. Baaz, A. Leitsch / Journal of Symbolic Computation, 41 (2006), 381 - 410
• Proof Transformation by CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / in: "MKM 2006", J.M. Borwein, W.M. Farmer (ed.); Springer, Berlin Heidelberg, 2006, 82 - 93

2005

• Abstracting from the Propositional Structure of First-Order Proofs / S. Hetzl, A. Leitsch / Talk: Paris-Vienna Workshop 2005, Paris; 2005-12-19
• Cut-Elimination: Experiments with CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / Talk: Second Florence-Vienna Workshop on Logic and Computation, Florenz; 2005-11-02 - 2005-11-05
• CERES in many-valued logics / A. Leitsch / Talk: Second Florence-Vienna Workshop on Logic and Computation, Florenz, Italien; 2005-11-02 - 2005-11-05
• Computational Analysis of Proofs / A. Leitsch / Talk: European Summer School in Logic Language and Information 2005, Edinburgh, U.K.; 2005-08-13 - 2005-08-20
• The Resolution Principle / A. Leitsch, C. Fermüller / in: "Handbook of Philosophical Logic, 2nd ed., Volume 12", D.M. Gabbay, F. Guenthner (ed.); Springer, Dordrecht, Netherlands, 2005, 87 - 173
• Cut-Elimination: Experiments with CERES / M. Baaz, S. Hetzl, A. Leitsch, Clemens Richter, H. Spohr / in: "LOgic for Programming, Artificial Intelligence, and Reasoning", issued by: Franz Baader, Andrei Voronkov; Springer, LNAI, Heidelberg, 2005, ISBN: 3-540-25236-3, 481 - 495
• Event-related Outputs of Computations in P Systems / M. Cavaliere, R. Freund, A. Leitsch, Gh. Paun / in: "Third Brainstorming Week on Membrane Computing", M.A. Gutiérrez-Naranjo, A. Riscos-Núñez, F.J. Romero-Campero, D. Sburlan (ed.); issued by: Research Group on Natural Computing, Sevilla University; Fénix Editora, Sevilla, 2005, 107 - 122
• CERES in many-valued logics / M. Baaz, A. Leitsch / in: "Logic for Programming, Artificial Intelligence, and Reasoning (LNAI 3452)", F. Baader, A. Voronkov (ed.); Springer, 2005, ISBN: 3-540-25236-3, 1 - 20
• Resolution Theorem Proving: a logical point of view / A. Leitsch / in: "Logic Colloquium '01", issued by: Matthias Baaz, Sy-David Friedman, Jan Krajicek; Association of Symbolic Logic, A K Peters, Ltd., Wellesley, Massachusetts, 2005, (invited), ISBN: 1-56881-247-7, 3 - 42
• CERES in Many-Valued Logics / A. Leitsch, M. Baaz / in: "Logic for Programming, Artificial Intelligence, and Reasoning", issued by: Franz Baader, Andrei Voronkov; Springer, LNAI, Heidelberg, 2005, (invited), ISBN: 3-540-25236-3, 1 - 20

2004

• CERES: Cut-elimination by Resolution / A. Leitsch / Talk: Paris-Vienna Workshop 2004 on Proof Systems, Paris (invited); 2004-12-13 - 2004-12-14
• CERES: Cut-Elimination by Resolution / A. Leitsch / Talk: Eingeladener Vortrag an Universitaet, Universitaet Utrecht, Niederlande; 2004-09-10
• Cut-Elimination by Resolution / A. Leitsch / Talk: First Vienna-Florence Workshop on Logic and Computation, Florence (invited); 2004-01-27 - 2004-01-31
• Automated Model Building / R. Caferra, A. Leitsch, N. Peltier / Kluwer Academic Publishers, Dordrecht, The Netherlands, 2004, ISBN: 1-4020-2652-8; 341 pages

2003

• Clause Evaluation over Herbrand Interpretations / A. Leitsch / Talk: Seminar on Deduction and Infinite-state Model Checking, Dagstuhl, Germany (invited); 2003-04-21 - 2003-04-25

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.

• Algorithmic Introduction of ∏2-Cut / Doctoral Thesis by M. Lettmann / Supervisor, Reviewer: A. Leitsch, M. Baaz; Institut für Logic and Computation, 2018; oral examination: 2018-10-30
• Applications of Higher-Order Cut-Elimination / Doctoral Thesis by M. Riener / Supervisor, Reviewer: A. Leitsch, C. Benzmüller; Institut für Computersprachen, 2018
• Ceres in aussagenlogischen Beweisschemata / Master Thesis by A. Condoluci / Supervisor: A. Leitsch; Institut für Computersprachen, 2016; final examination: 2016-10-07
• Cut-Elimination in Functional Higher-Order Logic / Master Thesis by N. Pona / Supervisor: A. Leitsch; Institut für Computersprachen, 2016; final examination: 2016-09-21
• Advances in Schematic Cut Elimination / Doctoral Thesis by D. Cerna / Supervisor, Reviewer: A. Leitsch, N. Peltier, G. Moser; Institut für Computersprachen, 2015; oral examination: 2015-04-14
• Preuves par induction dans le calcul de superposition / Doctoral Thesis by A. Kersani / Supervisor, Reviewer: A. Leitsch, N. Peltier; Universite de Grenoble, France, 2014; oral examination: 2014-10-30
• Cut-elimination by resolution in intuitionistic logic / Doctoral Thesis by G. Reis / Supervisor, Reviewer: A. Leitsch, R. Iemhoff; Institut für Computersprachen, 2014; oral examination: 2014-07-16
• Unification in Higher-order Resolution / Doctoral Thesis by T. Libal / Supervisor, Reviewer: A. Leitsch, M. Schmidt-Schauss; Institut für Computersprachen, 2013; oral examination: 2013-02-22
• CERES in Proof Schemata / Doctoral Thesis by M. Rukhaia / Supervisor, Reviewer: N. Peltier, A. Leitsch; Institut für Computersprachen E185/2, 2012; oral examination: 2012-12-17
• Automation of cut-elimination in proof schemata / Doctoral Thesis by T. Dunchev / Supervisor, Reviewer: A. Leitsch, N. Peltier; Institut für Computersprachen E185/2, 2012; oral examination: 2012-12-17
• Integrating Theories into Inference Systems / Master Thesis by M. Riener / Supervisor: A. Leitsch; Institut für Computersprachen, 2011; final examination: 2011-03-23
• Simplification of Herbrand Sequents / Master Thesis by T. Dunchev / Supervisor: A. Leitsch; Institut für Computersprachen E185/2, 2009; final examination: 2009-09-09
• CERES and Fast Cut-Elimination / Master Thesis by M. Rukhaia / Supervisor: A. Leitsch; Institut für Computersprachen E185/2, 2009; final examination: 2009-09-09
• A GeneralAnalysis of Cut-Elimination by CERES / Doctoral Thesis by B. Woltzenlogel-Paleo / Supervisor, Reviewer: A. Leitsch; Institut für Computersprachen E185/2, 2009; oral examination: 2009-08-28
• Cut-Elimination in Inductive Proofs of Weakly Quantified Theorems / Master Thesis by T. Libal / Supervisor: A. Leitsch; Institut für Computersprachen E185/2, 2008
• Characteristic Clause Sets and Proof Transformations / Doctoral Thesis by S. Hetzl / Supervisor, Reviewer: A. Leitsch, M. Baaz; Institut für Computersprachen E185/2, 2007; oral examination: 2007-06-14
• Proof Transformations by Resolution / Doctoral Thesis by Clemens Richter / Supervisor, Reviewer: A. Leitsch, M. Baaz; Institut für Computersprachen 185-2, 2006; oral examination: 2006-07-04