TU Wien Informatics

20 Years
Overview Professors Scientific Staff Administrative Staff Student Staff External Lecturers By Responsibilities By Committee By Name
Related
Guest Professors Honoraries Alumni (LinkedIn) #5qw

Alexander Leitsch

Univ.-Prof. i.R. Dr.phil.

Research Focus

  • Logic and Computation: 100%

Research Areas

  • automated deduction, proof theory

About

1) Automated deduction: Resolution decision procedures, decidable classes of first-order logic, automated model building, subsumption algorithms. 2) Proof theory: Analysis of cut elimination 3) Automated Lemma Generation 4) Proof Analysis

Role

Contact

2023W

2024S

 

2021

  • Schematic Refutations of Formula Schemata / Cerna, D. M., Leitsch, A., & Lolic, A. (2021). Schematic Refutations of Formula Schemata. Journal of Automated Reasoning, 65(5), 599–645. https://doi.org/10.1007/s10817-020-09583-8
    Download: PDF (683 KB)
  • An abstract form of the first epsilon theorem / Baaz, M., Leitsch, A., & Lolic, A. (2021). An abstract form of the first epsilon theorem. Journal of Logic and Computation, 30(8), 1447–1468. https://doi.org/10.1093/logcom/exaa044

2019

  • Extraction of Expansion Trees / Leitsch, A., & Lolic, A. (2019). Extraction of Expansion Trees. Journal of Automated Reasoning, 62(3), 393–430. https://doi.org/10.1007/s10817-018-9453-9
  • Schematic Refutations of Formula Schemata / Cerna, D., Leitsch, A., & Lolic, A. (2019). Schematic Refutations of Formula Schemata. arXiv. https://doi.org/10.48550/arXiv.1902.08055

2018

  • Extraction of Expansion Trees / Leitsch, A., & Lolic, A. (2018). Extraction of Expansion Trees. Journal of Automated Reasoning, 62(3), 393–430. https://doi.org/10.1007/s10817-018-9453-9
  • A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem / Leitsch, A., Baaz, M., & Lolic, A. (2018). A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. In Logical Foundations of Computer Science (pp. 55–71). Springer International Publishing AG. https://doi.org/10.1007/978-3-319-72056-2_4

2017

  • Ceres in intuitionistic logic / Cerna, D., Leitsch, A., Reis, G., & Wolfsteiner, S. P. (2017). Ceres in intuitionistic logic. Annals of Pure and Applied Logic, 168(10), 1783–1836. https://doi.org/10.1016/j.apal.2017.04.001
  • CERES for first-order schemata / Leitsch, A., Peltier, N., & Weller, D. (2017). CERES for first-order schemata. Journal of Logic and Computation, 27(7), 1897–1954. https://doi.org/10.1093/logcom/exx003
  • The problem of Pi_2-cut-introduction / Leitsch, A., & Lettmann, M. (2017). The problem of Pi_2-cut-introduction. Theoretical Computer Science, 706, 83–116. https://doi.org/10.1016/j.tcs.2017.10.003
  • Expansion Trees from Non-Normalized Proofs with CERES / Lolic, A., & Leitsch, A. (2017). Expansion Trees from Non-Normalized Proofs with CERES. Collegium Logicum Proof Theory: Herbrand’s Theorem Revisited, Wien, Austria. http://hdl.handle.net/20.500.12708/122275

2016

2015

2014

  • Cut-Elimination: Syntax and Semantics / Baaz, M., & Leitsch, A. (2014). Cut-Elimination: Syntax and Semantics. Studia Logica, 102(6), 1217–1244. https://doi.org/10.1007/s11225-014-9563-2
  • Introducing Quantified Cuts in Logic with Equality / Leitsch, A., Hetzl, S., Reis, G., & Weller, D. (2014). Introducing Quantified Cuts in Logic with Equality. arXiv. https://doi.org/10.48550/arXiv.1402.2474
  • Algorithmic introduction of quantified cuts / Hetzl, S., Leitsch, A., Reis, G., & Weller, D. (2014). Algorithmic introduction of quantified cuts. Theoretical Computer Science, 549, 1–16. https://doi.org/10.1016/j.tcs.2014.05.018
  • Mathematical Proof Analysis / Leitsch, A. (2014). Mathematical Proof Analysis. VSL 2014, Wien, Austria. http://hdl.handle.net/20.500.12708/85900
  • Introducing Quantified Cuts in Logic with Equality / Hetzl, S., Leitsch, A., Reis, G., Tapolczai, J., & Weller, D. (2014). Introducing Quantified Cuts in Logic with Equality. In Automated Reasoning (pp. 240–254). LNCS 8562. https://doi.org/10.1007/978-3-319-08587-6_17

2013

  • Ceres for First-Order Schemata / Leitsch, A., Dunchev, T., Weller, D., & Rukhaia, M. (2013). Ceres for First-Order Schemata (p. 40). arXiv. https://doi.org/10.48550/arXiv.1303.4257
  • Methods of Cut-Elimination / Leitsch, A. (2013). Methods of Cut-Elimination. Ninth International Tbilisi Summer School in Logic and Language, Tbilisi, Georgia, Non-EU. http://hdl.handle.net/20.500.12708/85688
  • A method of algorithmic cut-introduction / Leitsch, A. (2013). A method of algorithmic cut-introduction. Workshop on Skolemization, Utrecht, EU. http://hdl.handle.net/20.500.12708/85577
  • Prooftool: a GUI for the GAPT Framework / Leitsch, A., Libal, T., Riener, M., Weller, D., Woltzenlogel-Paleo, B., & Dunchev, T. (2013). Prooftool: a GUI for the GAPT Framework. In C. Kaliszyk (Ed.), Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/eptcs.118

2012

  • Towards Algorithmic Cut-Introduction / Leitsch, A., Hetzl, S., & Weller, D. (2012). Towards Algorithmic Cut-Introduction. In N. Bjørner & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 228–242). Springer LNCS. https://doi.org/10.1007/978-3-642-28717-6_19
  • CERES for First-Order Schemata / Leitsch, A. (2012). CERES for First-Order Schemata. Collegium Logicum 2012: Structural Proof Theory, Paris, France, EU. http://hdl.handle.net/20.500.12708/85552
  • Towards CERes in intuitionistic logic / Leitsch, A., Reis, G., & Woltzenlogel-Paleo, B. (2012). Towards CERes in intuitionistic logic. In P. Cegielski (Ed.), Computer Science Logic (CSL’12) - 26th International Workshop/21st (pp. 485–499). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. http://hdl.handle.net/20.500.12708/54225
  • System feature description: importing refutations into the GAPT framework / Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., & Woltzenlogel-Paleo, B. (2012). System feature description: importing refutations into the GAPT framework. In D. Pichardie & T. Weber (Eds.), Proceeding of Proof Exchange for Theorem Proving | Second International Workshop, PxTP 2012 (pp. 51–57). http://hdl.handle.net/20.500.12708/41146

2011

  • Ceres in higher-order logic / Hetzl, S., Leitsch, A., & Weller, D. (2011). Ceres in higher-order logic. Annals of Pure and Applied Logic, 162(12), 1001–1034. https://doi.org/10.1016/j.apal.2011.06.005
  • Towards algorithmic cut-introduction / Leitsch, A. (2011). Towards algorithmic cut-introduction. 2nd Workshop of the Joint Project “Structural and Computational Proof Theory,” Innsbruck, Austria. http://hdl.handle.net/20.500.12708/85174
  • Methods of Cut-Elimination / Baaz, M., & Leitsch, A. (2011). Methods of Cut-Elimination. Springer Verlag. https://doi.org/10.1007/978-94-007-0320-9

2010

  • Fast cut-elimination by CERES / Baaz, M., & Leitsch, A. (2010). Fast cut-elimination by CERES. In S. Feferman & W. Sieg (Eds.), Proofs, Categories and Computations, Essays in Honor of Grigori Mints (pp. 31–48). College Publications (Kings College). http://hdl.handle.net/20.500.12708/27039
  • Fast Cut-Elimination by CERES / Leitsch, A., & Baaz, M. (2010). Fast Cut-Elimination by CERES. In S. Feferman & W. Sieg (Eds.), Proofs, Categories and Computations (pp. 31–49). College Publications. http://hdl.handle.net/20.500.12708/27080
  • CERES in higher-order-logic / Hetzl, S., Leitsch, A., & Weller, D. (2010). CERES in higher-order-logic. Workshop on Classical Logic and Computation (CL&C’10), Brünn, EU. http://hdl.handle.net/20.500.12708/85096
  • CERES in higher-order-logic / Leitsch, A. (2010). CERES in higher-order-logic. Collegium Locicum 2010: Proofs and Structures, Paris, EU. http://hdl.handle.net/20.500.12708/85073
  • System Description: The Proof Transformation System CERES / Leitsch, A., Dunchev, T., Weller, D., Woltzenlogel-Paleo, B., & Libal, T. (2010). System Description: The Proof Transformation System CERES. In J. Giesl & R. Hähnle (Eds.), IJCAR 2010 (pp. 427–433). Springer, LNAI. http://hdl.handle.net/20.500.12708/53564

2009

  • A Clausal Approach to Proof Analysis in Second-Order Logic / Hetzl, S., Leitsch, A., Weller, D., & Woltzenlogel-Paleo, B. (2009). A Clausal Approach to Proof Analysis in Second-Order Logic. In A. Nerode & S. Artemov (Eds.), LFCS 2009: Logical Foundations of Computer Science (pp. 214–229). Springer, LNCS. https://doi.org/10.1007/978-3-540-92687-0_15
  • Fast Cut-Elimination by CERES / Leitsch, A. (2009). Fast Cut-Elimination by CERES. Moscow-Vienna Workshop on Logic and Computation 2009, Wien, Austria. http://hdl.handle.net/20.500.12708/84950

2008

  • How to Acknowledge Hypercomputation / Leitsch, A., Schachner, G., & Svozil, K. (2008). How to Acknowledge Hypercomputation. Complex Systems, 18, 131–143. http://hdl.handle.net/20.500.12708/170847
  • Towards an algorithmic construction of cut-elimination procedures / CIABATTONI, A., & LEITSCH, A. (2008). Towards an algorithmic construction of cut-elimination procedures. Mathematical Structures in Computer Science, 18(1), 81–105. https://doi.org/10.1017/s0960129507006573
  • CERES: An analysis of Fürstenberg's proof of the infinity of primes / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2008). CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Theoretical Computer Science, 403(2–3), 160–175. https://doi.org/10.1016/j.tcs.2008.02.043
  • CERES: Analysis of the fifth Proof of the Infinity of Primes / Leitsch, A. (2008). CERES: Analysis of the fifth Proof of the Infinity of Primes. Non-classical Logics: from Foundations to Applications, Pisa, EU. http://hdl.handle.net/20.500.12708/84789
  • Herbrand Sequent Extraction / Leitsch, A., Hetzl, S., Weller, D., & Woltzenlogel-Paleo, B. (2008). Herbrand Sequent Extraction. In S. Autexier (Ed.), AISC/Calculemus/MKM 2008 (pp. 462–477). Springer. http://hdl.handle.net/20.500.12708/52369
  • Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions / Leitsch, A., Hetzl, S., Weller, D., & Woltzenlogel-Paleo, B. (2008). Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions. In G. Sutcliffe, S. Colton, & S. Schulz (Eds.), Proceedings of the CICIM Workshops on ESARM-08 (pp. 23–41). CEUR-WS.org. http://hdl.handle.net/20.500.12708/52368
  • Transforming and Analyzing Proofs in the CERES-system / Leitsch, A., Hetzl, S., Weller, D., & Woltzenlogel-Paleo, B. (2008). Transforming and Analyzing Proofs in the CERES-system. In P. Rudnicki & G. Sutcliffe (Eds.), Proceedings of the LPAR 2008 Workshops (pp. 77–91). CEUR-WS.org. http://hdl.handle.net/20.500.12708/52364

2007

2006

  • System Description: The Cut-Elimination System CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2006). System Description: The Cut-Elimination System CERES. In G. Sutcliffe, R. Schmidt, & S. Schulz (Eds.), ESCoR 2006 Empirically Successful Computerized Reasoning (p. 9). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/176627
  • Proof transformation by CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2006). Proof transformation by CERES. Lecture Notes in Computer Science, 82–93. https://doi.org/10.1007/11812289_8
  • Towards a clausal analysis of cut-elimination / Baaz, M., & Leitsch, A. (2006). Towards a clausal analysis of cut-elimination. Journal of Symbolic Computation, 41, 381–410. http://hdl.handle.net/20.500.12708/172032
  • CERES: Cut-Elimination by Resolution / Leitsch, A. (2006). CERES: Cut-Elimination by Resolution. MANYVAL 06, Gargnano, EU. http://hdl.handle.net/20.500.12708/84555
  • Proof Transformation by CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2006). Proof Transformation by CERES. In J. M. Borwein & W. Farmer (Eds.), MKM 2006 (pp. 82–93). Springer. http://hdl.handle.net/20.500.12708/51679

2005

  • The Resolution Principle / Leitsch, A., & Fermüller, C. (2005). The Resolution Principle. In D. M. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic, 2nd ed., Volume 12 (pp. 87–173). Springer. http://hdl.handle.net/20.500.12708/25357
  • Abstracting from the Propositional Structure of First-Order Proofs / Hetzl, S., & Leitsch, A. (2005). Abstracting from the Propositional Structure of First-Order Proofs. Paris-Vienna Workshop 2005, Paris, EU. http://hdl.handle.net/20.500.12708/84469
  • Cut-Elimination: Experiments with CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2005). Cut-Elimination: Experiments with CERES. Second Florence-Vienna Workshop on Logic and Computation, Florence, Italy, Austria. http://hdl.handle.net/20.500.12708/84468
  • CERES in many-valued logics / Leitsch, A. (2005). CERES in many-valued logics. Second Florence-Vienna Workshop on Logic and Computation, Florence, Italy, Austria. http://hdl.handle.net/20.500.12708/84460
  • Computational Analysis of Proofs / Leitsch, A. (2005). Computational Analysis of Proofs. European Summer School in Logic Language and Information 2005, Edinburgh, U.K., EU. http://hdl.handle.net/20.500.12708/84459
  • Event-related Outputs of Computations in P Systems / Cavaliere, M., Freund, R., Leitsch, A., & Paun, G. (2005). Event-related Outputs of Computations in P Systems. In M. A. Gutiérrez-Naranjo, A. Riscos-Núñez, F. J. Romero-Campero, & D. Sburlan (Eds.), Third Brainstorming Week on Membrane Computing (pp. 107–122). Fénix Editora. http://hdl.handle.net/20.500.12708/51149
  • Resolution Theorem Proving: a logical point of view / Leitsch, A. (2005). Resolution Theorem Proving: a logical point of view. In Logic Colloquium ’01 (pp. 3–42). Association of Symbolic Logic, A K Peters, Ltd. http://hdl.handle.net/20.500.12708/51012
  • Cut-Elimination: Experiments with CERES / Baaz, M., Hetzl, S., Leitsch, A., Richter, C., & Spohr, H. (2005). Cut-Elimination: Experiments with CERES. In LOgic for Programming, Artificial Intelligence, and Reasoning (pp. 481–495). Springer, LNAI. http://hdl.handle.net/20.500.12708/51011
  • CERES in Many-Valued Logics / Leitsch, A., & Baaz, M. (2005). CERES in Many-Valued Logics. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 1–20). Springer, LNAI. http://hdl.handle.net/20.500.12708/51010
  • CERES in many-valued logics / Baaz, M., & Leitsch, A. (2005). CERES in many-valued logics. In F. Baader & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (LNAI 3452) (pp. 1–20). Springer. http://hdl.handle.net/20.500.12708/40591

2004

  • CERES: Cut-Elimination by Resolution / Leitsch, A. (2004). CERES: Cut-Elimination by Resolution. Eingeladener Vortrag an Universitaet, Universitaet Utrecht, Niederlande, Austria. http://hdl.handle.net/20.500.12708/84384
  • CERES: Cut-elimination by Resolution / Leitsch, A. (2004). CERES: Cut-elimination by Resolution. Paris-Vienna Workshop 2004 on Proof Systems, Paris, Austria. http://hdl.handle.net/20.500.12708/84383
  • Cut-Elimination by Resolution / Leitsch, A. (2004). Cut-Elimination by Resolution. First Vienna-Florence Workshop on Logic and Computation, Florence, Austria. http://hdl.handle.net/20.500.12708/84382

2003

  • Clause Evaluation over Herbrand Interpretations / Leitsch, A. (2003). Clause Evaluation over Herbrand Interpretations. Seminar on Deduction and Infinite-state Model Checking, Dagstuhl, Germany, Austria. http://hdl.handle.net/20.500.12708/84261

 

2020

  • Automated proof analysis by CERES / Lolić, A. (2020). Automated proof analysis by CERES [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.47184
    Download: PDF (1.59 MB)

2018

2017

2016

2015

2014

2012

  • Unification in higher-order resolution / Líbal, T. (2012). Unification in higher-order resolution [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-57326
    Download: PDF (792 KB)
  • Automation of cut-elimination in proof schemata / Dunchev, T. C. (2012). Automation of cut-elimination in proof schemata [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-49478
    Download: PDF (741 KB)
  • Models of hypercomputation / Acar, E. (2012). Models of hypercomputation [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-52279
    Download: PDF (917 KB)
  • CERES in proof schemata / Rukhaia, M. (2012). CERES in proof schemata [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/160038

2011

2010

  • CERES in higher-order logic / Weller, D. (2010). CERES in higher-order logic [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/159952

2009

  • A general analysis of cut-elimination by CERes / Woltzenlogel Paleo, B. (2009). A general analysis of cut-elimination by CERes [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-32321
    Download: PDF (1.38 MB)
  • Simplification of Herbrand sequents / Dunchev, T. C. (2009). Simplification of Herbrand sequents [Master Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-37482
    Download: PDF (310 KB)
  • CERES and fast cut-elimination / Rukhaia, M. (2009). CERES and fast cut-elimination [Master Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/186564

2008

2007

  • Herbrand sequent extraction / Woltzenlogel-Paleo, B. (2007). Herbrand sequent extraction [Master Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-18086
    Download: PDF (481 KB)
  • Characteristic clause sets and proof transformations / Hetzl, S. (2007). Characteristic clause sets and proof transformations [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/183195

2006

2005

  • A proof tool for Gentzen Calculi / Spohr, H. (2005). A proof tool for Gentzen Calculi [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/184620

2004

2003