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

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

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

Ebner, G., Hetzl, S., Leitsch, A., Reis, G., & Weller, D. (2019). On the Generation of Quantified Lemmas. Journal of Automated Reasoning, 63, 95–126. https://doi.org/10.1007/s10817-018-9462-8 ( reposiTUm)

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

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

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

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

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

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

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

Leitsch, A., Schachner, G., & Svozil, K. (2008). How to Acknowledge Hypercomputation. Complex Systems, 18, 131–143. http://hdl.handle.net/20.500.12708/170847 ( reposiTUm)

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

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

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

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

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

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). ( reposiTUm)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Baaz, M., & Leitsch, A. (2011). Methods of Cut-Elimination. Springer Verlag. https://doi.org/10.1007/978-94-007-0320-9 ( reposiTUm)

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

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

Leitsch, A. (2016). CERES in intuitionistic logic completeness. Magica 16, Mailand, Italy. http://hdl.handle.net/20.500.12708/86314 ( reposiTUm)

Leitsch, A. (2014). Mathematical Proof Analysis. VSL 2014, Wien, Austria. http://hdl.handle.net/20.500.12708/85900 ( reposiTUm)

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

Leitsch, A. (2013). A method of algorithmic cut-introduction. Workshop on Skolemization, Utrecht, EU. http://hdl.handle.net/20.500.12708/85577 ( reposiTUm)

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

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

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

Leitsch, A. (2010). CERES in higher-order-logic. Collegium Locicum 2010: Proofs and Structures, Paris, EU. http://hdl.handle.net/20.500.12708/85073 ( reposiTUm)

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

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

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

Leitsch, A. (2006). CERES: Cut-Elimination by Resolution. MANYVAL 06, Gargnano, EU. http://hdl.handle.net/20.500.12708/84555 ( reposiTUm)

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

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

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

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

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

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

Leitsch, A. (2004). CERES: Cut-Elimination by Resolution. Eingeladener Vortrag an Universitaet, Universitaet Utrecht, Niederlande, Austria. http://hdl.handle.net/20.500.12708/84384 ( reposiTUm)

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

Cerna, D., Leitsch, A., & Lolic, A. (2019). Schematic Refutations of Formula Schemata. arXiv. https://doi.org/10.48550/arXiv.1902.08055 ( reposiTUm)

Leitsch, A., & Cerna, D. (2016). Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]. arXiv. https://doi.org/10.48550/arXiv.1601.06548 ( reposiTUm)

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

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

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