About

1) Automated deduction: Resolution decision procedures, decidable classesof first-order logic, automated model building, subsumption algorithms.2) Proof theory: Analysis of cut elimination3) Automated Lemma Generation4) Proof Analysis

Role

Retired Professor
Theory and Logic, E192-05

Contact

Courses

2024W

Bachelor Thesis for Informatics and Business Informatics / 185.A26 / PR
Higher-order Logic / 192.040 / VU

2025S

Bachelor Thesis for Informatics and Business Informatics / 185.A26 / PR

Projects

Algorithmic Structuring and Compression of Proofs
2013 – 2016 / Austrian Science Fund (FWF)
Publication: 149881
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)
Publications: 53859 / 85196
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)

Publications

2024

Herbrand's theorem for inductive proofs / Leitsch, A., & Mahler, S. (2024, June 25). Herbrand’s theorem for inductive proofs [Conference Presentation]. Logic Colloquium 2024, Göteburg, Sweden. http://hdl.handle.net/20.500.12708/211184
On Proof Schemata and Primitive Recursive Arithmetic / Leitsch, A., Lolic, A., & Mahler, S. L. (2024). On Proof Schemata and Primitive Recursive Arithmetic. In N. Bjorner, M. Heule, & A. Voronkov (Eds.), LPAR 2024 Complementary Volume (pp. 117–130). https://doi.org/10.29007/4g2q
Project: Pandaforest (2022–2025)
Towards an Analysis of Proofs in Arithmetic / Leitsch, A., Lolić, A., & Mahler, S. (2024). Towards an Analysis of Proofs in Arithmetic. In C. Kop (Ed.), 19th International Workshop on Logical and Semantic Frameworks, with Applications. LSFA 2024 Proceedings (pp. 122–135).
Project: Pandaforest (2022–2025)
Herbrand's Theorem in Inductive Proofs / Leitsch, A., & Lolic, A. (2024). Herbrand’s Theorem in Inductive Proofs. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 295–310). EasyChair. https://doi.org/10.29007/dwdf
Project: Pandaforest (2022–2025)

2021

Schematic Refutations of Formula Schemata / Cerna, D. M., Leitsch, A., & Lolić, 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

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

2018

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

Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version] / Leitsch, A., & Cerna, D. (2016). Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]. arXiv. https://doi.org/10.48550/arXiv.1601.06548
Schematic Cut Elimination and the Ordered Pigeonhole Principle / Leitsch, A., & Cerna, D. (2016). Schematic Cut Elimination and the Ordered Pigeonhole Principle. In N. Olivetti (Ed.), Automated Reasoning - 8th International Joint Conference, {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings (pp. 241–256). http://hdl.handle.net/20.500.12708/56560
CERES in intuitionistic logic completeness / Leitsch, A. (2016). CERES in intuitionistic logic completeness. Magica 16, Mailand, Italy. http://hdl.handle.net/20.500.12708/86314

2015

A Note on the Complexity of Classical and Intuitionistic Proofs / Leitsch, A., Baaz, M., & Reis, G. (2015). A Note on the Complexity of Classical and Intuitionistic Proofs. In Logic in Computer Science (LICS) (pp. 657–666). http://hdl.handle.net/20.500.12708/56144
Analysis of Clause set Schema Aided by Automated Theorem Proving: {A} Case Study [Extended Paper] / Leitsch, A., & Cerna, D. (2015). Analysis of Clause set Schema Aided by Automated Theorem Proving: {A} Case Study [Extended Paper]. arXiv. https://doi.org/10.48550/arXiv.1503.08551

2014

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

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

Proof Transformations and Structural Invariance / Leitsch, A., & Hetzl, S. (2007). Proof Transformations and Structural Invariance. In S. Aguzzoli (Ed.), LNAI 4460: Algebraic and Proof-theoretic Aspects (pp. 201–230). Springer, LNAI 4460. http://hdl.handle.net/20.500.12708/25413
CERES: An analysis of Fürstenberg's proof of the infinity of primes / Leitsch, A. (2007). CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Moscow-Vienna Workshop on Logic and Computation, Moscow, Austria. http://hdl.handle.net/20.500.12708/84650

2006

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

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

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

Supervisions

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

Extracting programs from proofs : using Friedman's A-translation and realizability / Rietdijk, M. (2018). Extracting programs from proofs : using Friedman’s A-translation and realizability [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.52485
Download: PDF (611 KB)
Algorithmic introduction of π2-cuts / Lettmann, M. P. (2018). Algorithmic introduction of π2-cuts [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.60480
Download: PDF (1.78 MB)

2017

Preprocessing in higher-order reasoning : learning from QBF solving / Schurr, H. J. (2017). Preprocessing in higher-order reasoning : learning from QBF solving [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2017.36282
Download: PDF (621 KB)
Applications of higher-order cut-elimination / Riener, M. (2017). Applications of higher-order cut-elimination [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2017.25064
Download: PDF (7.03 MB)

2016

Schnittelimination in funktionaler Logik höherer Stufe / Pona, N. (2016). Schnittelimination in funktionaler Logik höherer Stufe [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.37392
Download: PDF (723 KB)
CERES in aussagenlogischen Beweisschemata / Condoluci, A. (2016). CERES in aussagenlogischen Beweisschemata [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/79071

2015

Herbrand Sequente und die skolemisierungs-freie CERES Methode / Lolić, A. (2015). Herbrand Sequente und die skolemisierungs-freie CERES Methode [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.28745
Download: PDF (480 KB)
Structural analysis of cut-elimination / Wolfsteiner, S. P. (2015). Structural analysis of cut-elimination [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.25878
Download: PDF (913 KB)
Algorithms for quantified cut-introduction / Spörk, C. W. (2015). Algorithms for quantified cut-introduction [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.24545
Download: PDF (928 KB)
Advances in schematic cut elimination / Cerna, D. M. (2015). Advances in schematic cut elimination [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.25063
Download: PDF (1.31 MB)

2014

Space & congruence compression of proofs / Fellner, A. (2014). Space & congruence compression of proofs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.24717
Download: PDF (822 KB)
Cut-elimination by resolution in intuitionistic logic / Machado Nogueira Reis, G. (2014). Cut-elimination by resolution in intuitionistic logic [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.23308
Download: PDF (923 KB)

2012

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

Integrating theories into inference systems / Riener, M. (2011). Integrating theories into inference systems [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/159961

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

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

Cut elimination in inductive proofs of weakly quantified theorems / Libal, T. (2008). Cut elimination in inductive proofs of weakly quantified theorems [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-26492
Download: PDF (483 KB)

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

Proof transformations by resolution : computational methods of cut-elimination / Richter, C. (2006). Proof transformations by resolution : computational methods of cut-elimination [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-19752
Download: PDF (591 KB)

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

Projection-based cut-elimination and normalization / Hetzl, S. (2004). Projection-based cut-elimination and normalization [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-10645
Download: PDF (338 KB)
Arithmetical and subrecursive hierarchies / Holzinger, W. (2004). Arithmetical and subrecursive hierarchies [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/182590

2003

Diagonalization and self-application : applications in logic and computer science / Richter, C. (2003). Diagonalization and self-application : applications in logic and computer science [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/185810

Related

Alexander Leitsch

Research Focus

Research Areas

About

Role

Contact

Courses

2024W

2025S

Projects

Publications

2024

2021

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

Supervisions

2020

2018

2017

2016

2015

2014

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003