2019W

• Research Seminar LogiCS / SE / 184.767

2020S

• Research Seminar LogiCS / SE / 184.767

 

• 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)

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)

2018

• Extraction of Expansion Trees / A. Lolic, A. Leitsch / Journal of Automated Reasoning, 61 (2018), 1; 1 - 38
• 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

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 / CoRR - Computing Research Repository, abs/1601.06548 (2016), abs/1601.06548
• 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

2015

• 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
• 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

2014

• Mathematical Proof Analysis / A. Leitsch / Keynote Lecture: VSL 2014, Wien; 2014-07-12 - 2014-07-26
• Algorithmic introduction of quantified cuts / S. Hetzl, A. Leitsch, G. Reis, D. Weller / Theoretical Computer Science, 549 (2014), 1 - 16
• Cut-Elimination: Syntax and Semantics / M. Baaz, A. Leitsch / Studia Logica, 102 (2014), 6; 1217 - 1244
• 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
• 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
• 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

2012

• CERES for First-Order Schemata / A. Leitsch / Talk: Collegium Logicum 2012: Structural Proof Theory, Paris, France; 2012-11-15 - 2012-11-16
• 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
• 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

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 / in: "Lecture Notes in Computer Science, 5407", E. Artemov, A. Nerode (ed.); Springer LNCS, Heidelberg, 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 / 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

2008

• 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
• 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

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

• 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
• 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

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

 

• Algorithmic Introduction of ∏2-Cut / PhD 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 / PhD Thesis by M. Riener / Supervisor, Reviewer: A. Leitsch, C. Benzmüller; Institut für Computersprachen, 2018
• 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
• Ceres in aussagenlogischen Beweisschemata / Master Thesis by A. Condoluci / Supervisor: A. Leitsch; Institut für Computersprachen, 2016; final examination: 2016-10-07
• Advances in Schematic Cut Elimination / PhD 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 / PhD 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 / PhD 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 / PhD 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 / PhD 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 / PhD 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
• A GeneralAnalysis of Cut-Elimination by CERES / PhD Thesis by B. Woltzenlogel-Paleo / Supervisor, Reviewer: A. Leitsch; Institut für Computersprachen E185/2, 2009; oral examination: 2009-08-28
• 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
• 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 / PhD 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 / PhD Thesis by Clemens Richter / Supervisor, Reviewer: A. Leitsch, M. Baaz; Institut für Computersprachen 185-2, 2006; oral examination: 2006-07-04