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
-
Retired Professor
Theory and Logic, E192-05
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
-
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) -
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, EU. http://hdl.handle.net/20.500.12708/86314
2015
- 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
- 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
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
- 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
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
-
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) -
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) - 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