Edit Profile (opens in new tab) Leitsch, Alexander Co-Author Distance Author ID: leitsch.alexander Published as: Leitsch, Alexander; Leitsch, A. Documents Indexed: 72 Publications since 1978, including 3 Books and 1 Additional arXiv Preprint 4 Contributions as Editor Reviewing Activity: 39 Reviews Co-Authors: 35 Co-Authors with 58 Joint Publications 775 Co-Co-Authors all top 5 Co-Authors 18 single-authored 24 Baaz, Matthias 11 Hetzl, Stefan 10 Weller, Daniel S. 6 Reis, Giselle 5 Fermüller, Christian G. 5 Lolic, Anela 4 Gottlob, Georg 4 Woltzenlogel Paleo, Bruno 3 Cerna, David M. 3 Richter, Clemens 3 Spohr, Hendrik 2 Egly, Uwe 2 Ettl, Wolfgang 2 Mundici, Daniele 2 Peltier, Nicolas 2 Tammet, Tanel 1 Caferra, Ricardo 1 Cavaliere, Matteo 1 Ciabattoni, Agata 1 Dunchev, Cvetan 1 Dunchev, Tsvetan 1 Ebner, Gabriel 1 Freund, Rudolf 1 Goré, Rajeev Prabhakar 1 Hustadt, Ullrich 1 Lettmann, Michael Peter 1 Libal, Tomer 1 Nipkow, Tobias 1 Păun, Gheorghe 1 Schachner, Günter 1 Svozil, Karl 1 Tapolczai, Janos 1 Wolfsteiner, Simon 1 Zach, Richard 1 Zamov, Nail Kalimatovitch all top 5 Serials 6 Sitzungsberichte. Abteilung II. Österreichische Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse 4 Theoretical Computer Science 4 Annals of Pure and Applied Logic 4 Lecture Notes in Computer Science 3 Annales Societatis Mathematicae Polonae. Series IV 3 Journal of Automated Reasoning 3 Journal of Logic and Computation 2 Journal of Symbolic Computation 1 Computing 1 Journal of the Association for Computing Machinery 1 Studia Logica 1 Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 1 Complex Systems 1 MSCS. Mathematical Structures in Computer Science 1 International Journal of Computer Mathematics 1 Journal of Automata, Languages and Combinatorics 1 Logic Journal of the IGPL 1 Applied Logic Series 1 Trends in Logic – Studia Logica Library all top 5 Fields 62 Mathematical logic and foundations (03-XX) 49 Computer science (68-XX) 3 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Group theory and generalizations (20-XX) 1 Probability theory and stochastic processes (60-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 57 Publications have been cited 436 times in 207 Documents Cited by ▼ Year ▼ Resolution decision procedures. Zbl 0993.68119 Fermüller, Christian G.; Leitsch, Alexander; Hustadt, Ullrich; Tammet, Tanel 31 2001 The resolution calculus. Zbl 0867.68095 Leitsch, Alexander 28 1997 Cut-elimination and redundancy-elimination by resolution. Zbl 0976.03059 Baaz, Matthias; Leitsch, Alexander 26 2000 On Skolemization and proof complexity. Zbl 0815.03003 Baaz, Matthias; Leitsch, Alexander 26 1994 Resolution methods for the decision problem. Zbl 0789.03013 22 1993 Hyperresolution and automated model building. Zbl 0861.68086 Fermüller, Christian; Leitsch, Alexander 20 1996 Herbrand sequent extraction. Zbl 1166.68347 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno 17 2008 Automated model building. Zbl 1085.03009 Caferra, Ricardo; Leitsch, Alexander; Peltier, Nicholas 17 2004 Normal form transformations. Zbl 1005.03013 Baaz, Matthias; Egly, Uwe; Leitsch, Alexander 16 2001 On the efficiency of subsumption algorithms. Zbl 0633.68028 Gottlob, G.; Leitsch, A. 15 1985 Cut normal forms and proof complexity. Zbl 0940.03062 Baaz, Matthias; Leitsch, Alexander 15 1999 Algorithmic introduction of quantified cuts. Zbl 1393.03050 Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel 15 2014 Towards algorithmic cut-introduction. Zbl 1352.68213 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel 14 2012 CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Zbl 1181.68264 Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik 14 2008 Cut-elimination: experiments with CERES. Zbl 1108.03305 Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik 12 2005 Methods of cut-elimination. Zbl 1225.03075 Baaz, Matthias; Leitsch, Alexander 12 2011 Decision procedures and model building in equational clause logic. Zbl 0903.03010 Fermüller, Christian G.; Leitsch, Alexander 10 1998 Introducing quantified cuts in logic with equality. Zbl 1423.68418 Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel 10 2014 Towards a clausal analysis of cut-elimination. Zbl 1125.03013 Baaz, Matthias; Leitsch, Alexander 9 2006 Proof transformation by CERES. Zbl 1125.03012 Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik 8 2006 Deciding clause classes by semantic clash resolution. Zbl 0789.03016 Leitsch, Alexander 8 1993 On different concepts of resolution. Zbl 0646.03011 Leitsch, Alexander 7 1989 Complexity of resolution proofs and function introduction. Zbl 0769.03009 Baaz, Matthias; Leitsch, Alexander 6 1992 Completeness of a first-order temporal logic with time-gaps. Zbl 0872.68171 Baaz, Matthias; Leitsch, Alexander; Zach, Richard 6 1996 CERES in higher-order logic. Zbl 1259.03071 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel 5 2011 Model building by resolution. Zbl 0788.68128 Fermüller, Christian G.; Leitsch, Alexander 5 1993 Cut-elimination and proof schemata. Zbl 1326.03069 Dunchev, Cvetan; Leitsch, Alexander; Rukhaia, Mikheil; Weller, Daniel 5 2015 Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Zbl 0968.00052 4 2001 Fast subsumption algorithms. Zbl 0588.68044 Gottlob, G.; Leitsch, A. 4 1985 Towards an algorithmic construction of cut-elimination procedures. Zbl 1138.03043 Ciabattoni, Agata; Leitsch, Alexander 3 2008 Decision-algorithms for the associativity of Latin squares. Zbl 0509.05022 Leitsch, A. 3 1983 Proof transformations and structural invariance. Zbl 1123.03050 Hetzl, Stefan; Leitsch, Alexander 3 2007 Deciding Horn classes by hyperresolution. Zbl 0925.03056 Leitsch, Alexander 3 1990 CERES in many-valued logics. Zbl 1109.03007 Baaz, Matthias; Leitsch, Alexander 3 2005 A clausal approach to proof analysis in second-order logic. Zbl 1211.03018 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno 3 2009 Decision procedures and model building or how to improve logical information in automated deduction. Zbl 0966.03011 Leitsch, Alexander 2 2000 Methods of functional extension. Zbl 0840.03042 Baaz, Matthias; Leitsch, Alexander 2 1995 A sequent-calculus based formulation of the extended first epsilon theorem. Zbl 1503.03044 Baaz, Matthias; Leitsch, Alexander; Lolic, Anela 2 2018 Fast cut-elimination by projection. Zbl 0889.03048 Baaz, Matthias; Leitsch, Alexander 2 1997 The problem of \(\Pi_{2}\)-cut-introduction. Zbl 1423.03240 Leitsch, Alexander; Lettmann, Michael 2 2018 Cut-elimination: syntax and semantics. Zbl 1354.03086 Baaz, M.; Leitsch, A. 2 2014 Extraction of expansion trees. Zbl 1468.68296 Leitsch, Alexander; Lolic, Anela 2 2019 On the generation of quantified lemmas. Zbl 1459.03011 Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel 2 2019 Schematic cut elimination and the ordered pigeonhole principle. Zbl 1476.03079 Cerna, David M.; Leitsch, Alexander 2 2016 Implication algorithms for classes of Horn clauses. Zbl 0679.68172 Leitsch, A. 1 1989 Strong splitting rules in automated theorem proving. Zbl 1209.68503 Baaz, Matthias; Leitsch, Alexander 1 1989 Fast cut-elimination by CERES. Zbl 1221.03057 Baaz, Matthias; Leitsch, Alexander 1 2010 On some formal problems in resolution theorem proving. Zbl 0689.03004 Leitsch, Alexander 1 1988 CERES for first-order schemata. Zbl 1405.03089 Leitsch, Alexander; Peltier, Nicolas; Weller, Daniel 1 2017 Comparing the complexity of cut-elimination methods. Zbl 1024.03058 Baaz, Matthias; Leitsch, Alexander 1 2001 Die Anwendung starker Reduktionsregeln in automatischen Beweisen. Zbl 0596.03007 Baaz, Matthias; Leitsch, Alexander 1 1985 Eine Methode zur automatischen Problemreduktion. Zbl 0607.68071 Baaz, M.; Leitsch, A. 1 1985 Computational logic and proof theory. 5th Kurt Gödel Colloquium, KGC ’97. Vienna, Austria. August 25–29, 1997. Proceedings. Zbl 0870.00023 1 1997 Computational logic and proof theory. 3rd Kurt Gödel Colloquium, KGC ’93, Brno, Czech Republic, August 24–27, 1993. Proceedings. Zbl 0866.00036 1 1993 Towards CERes in intuitionistic logic. Zbl 1252.03124 Leitsch, Alexander; Reis, Giselle; Woltzenlogel Paleo, Bruno 1 2012 System description: the proof transformation system CERES. Zbl 1291.68338 Dunchev, Tsvetan; Leitsch, Alexander; Libal, Tomer; Weller, Daniel; Woltzenlogel Paleo, Bruno 1 2010 On proof mining by cut-elimination. Zbl 1431.03074 Leitsch, Alexander 1 2015 Extraction of expansion trees. Zbl 1468.68296 Leitsch, Alexander; Lolic, Anela 2 2019 On the generation of quantified lemmas. Zbl 1459.03011 Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel 2 2019 A sequent-calculus based formulation of the extended first epsilon theorem. Zbl 1503.03044 Baaz, Matthias; Leitsch, Alexander; Lolic, Anela 2 2018 The problem of \(\Pi_{2}\)-cut-introduction. Zbl 1423.03240 Leitsch, Alexander; Lettmann, Michael 2 2018 CERES for first-order schemata. Zbl 1405.03089 Leitsch, Alexander; Peltier, Nicolas; Weller, Daniel 1 2017 Schematic cut elimination and the ordered pigeonhole principle. Zbl 1476.03079 Cerna, David M.; Leitsch, Alexander 2 2016 Cut-elimination and proof schemata. Zbl 1326.03069 Dunchev, Cvetan; Leitsch, Alexander; Rukhaia, Mikheil; Weller, Daniel 5 2015 On proof mining by cut-elimination. Zbl 1431.03074 Leitsch, Alexander 1 2015 Algorithmic introduction of quantified cuts. Zbl 1393.03050 Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel 15 2014 Introducing quantified cuts in logic with equality. Zbl 1423.68418 Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel 10 2014 Cut-elimination: syntax and semantics. Zbl 1354.03086 Baaz, M.; Leitsch, A. 2 2014 Towards algorithmic cut-introduction. Zbl 1352.68213 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel 14 2012 Towards CERes in intuitionistic logic. Zbl 1252.03124 Leitsch, Alexander; Reis, Giselle; Woltzenlogel Paleo, Bruno 1 2012 Methods of cut-elimination. Zbl 1225.03075 Baaz, Matthias; Leitsch, Alexander 12 2011 CERES in higher-order logic. Zbl 1259.03071 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel 5 2011 Fast cut-elimination by CERES. Zbl 1221.03057 Baaz, Matthias; Leitsch, Alexander 1 2010 System description: the proof transformation system CERES. Zbl 1291.68338 Dunchev, Tsvetan; Leitsch, Alexander; Libal, Tomer; Weller, Daniel; Woltzenlogel Paleo, Bruno 1 2010 A clausal approach to proof analysis in second-order logic. Zbl 1211.03018 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno 3 2009 Herbrand sequent extraction. Zbl 1166.68347 Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno 17 2008 CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Zbl 1181.68264 Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik 14 2008 Towards an algorithmic construction of cut-elimination procedures. Zbl 1138.03043 Ciabattoni, Agata; Leitsch, Alexander 3 2008 Proof transformations and structural invariance. Zbl 1123.03050 Hetzl, Stefan; Leitsch, Alexander 3 2007 Towards a clausal analysis of cut-elimination. Zbl 1125.03013 Baaz, Matthias; Leitsch, Alexander 9 2006 Proof transformation by CERES. Zbl 1125.03012 Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik 8 2006 Cut-elimination: experiments with CERES. Zbl 1108.03305 Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik 12 2005 CERES in many-valued logics. Zbl 1109.03007 Baaz, Matthias; Leitsch, Alexander 3 2005 Automated model building. Zbl 1085.03009 Caferra, Ricardo; Leitsch, Alexander; Peltier, Nicholas 17 2004 Resolution decision procedures. Zbl 0993.68119 Fermüller, Christian G.; Leitsch, Alexander; Hustadt, Ullrich; Tammet, Tanel 31 2001 Normal form transformations. Zbl 1005.03013 Baaz, Matthias; Egly, Uwe; Leitsch, Alexander 16 2001 Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Zbl 0968.00052 4 2001 Comparing the complexity of cut-elimination methods. Zbl 1024.03058 Baaz, Matthias; Leitsch, Alexander 1 2001 Cut-elimination and redundancy-elimination by resolution. Zbl 0976.03059 Baaz, Matthias; Leitsch, Alexander 26 2000 Decision procedures and model building or how to improve logical information in automated deduction. Zbl 0966.03011 Leitsch, Alexander 2 2000 Cut normal forms and proof complexity. Zbl 0940.03062 Baaz, Matthias; Leitsch, Alexander 15 1999 Decision procedures and model building in equational clause logic. Zbl 0903.03010 Fermüller, Christian G.; Leitsch, Alexander 10 1998 The resolution calculus. Zbl 0867.68095 Leitsch, Alexander 28 1997 Fast cut-elimination by projection. Zbl 0889.03048 Baaz, Matthias; Leitsch, Alexander 2 1997 Computational logic and proof theory. 5th Kurt Gödel Colloquium, KGC ’97. Vienna, Austria. August 25–29, 1997. Proceedings. Zbl 0870.00023 1 1997 Hyperresolution and automated model building. Zbl 0861.68086 Fermüller, Christian; Leitsch, Alexander 20 1996 Completeness of a first-order temporal logic with time-gaps. Zbl 0872.68171 Baaz, Matthias; Leitsch, Alexander; Zach, Richard 6 1996 Methods of functional extension. Zbl 0840.03042 Baaz, Matthias; Leitsch, Alexander 2 1995 On Skolemization and proof complexity. Zbl 0815.03003 Baaz, Matthias; Leitsch, Alexander 26 1994 Resolution methods for the decision problem. Zbl 0789.03013 22 1993 Deciding clause classes by semantic clash resolution. Zbl 0789.03016 Leitsch, Alexander 8 1993 Model building by resolution. Zbl 0788.68128 Fermüller, Christian G.; Leitsch, Alexander 5 1993 Computational logic and proof theory. 3rd Kurt Gödel Colloquium, KGC ’93, Brno, Czech Republic, August 24–27, 1993. Proceedings. Zbl 0866.00036 1 1993 Complexity of resolution proofs and function introduction. Zbl 0769.03009 Baaz, Matthias; Leitsch, Alexander 6 1992 Deciding Horn classes by hyperresolution. Zbl 0925.03056 Leitsch, Alexander 3 1990 On different concepts of resolution. Zbl 0646.03011 Leitsch, Alexander 7 1989 Implication algorithms for classes of Horn clauses. Zbl 0679.68172 Leitsch, A. 1 1989 Strong splitting rules in automated theorem proving. Zbl 1209.68503 Baaz, Matthias; Leitsch, Alexander 1 1989 On some formal problems in resolution theorem proving. Zbl 0689.03004 Leitsch, Alexander 1 1988 On the efficiency of subsumption algorithms. Zbl 0633.68028 Gottlob, G.; Leitsch, A. 15 1985 Fast subsumption algorithms. Zbl 0588.68044 Gottlob, G.; Leitsch, A. 4 1985 Die Anwendung starker Reduktionsregeln in automatischen Beweisen. Zbl 0596.03007 Baaz, Matthias; Leitsch, Alexander 1 1985 Eine Methode zur automatischen Problemreduktion. Zbl 0607.68071 Baaz, M.; Leitsch, A. 1 1985 Decision-algorithms for the associativity of Latin squares. Zbl 0509.05022 Leitsch, A. 3 1983 all cited Publications top 5 cited Publications all top 5 Cited by 203 Authors 20 Hetzl, Stefan 20 Leitsch, Alexander 19 Baaz, Matthias 14 Peltier, Nicolas 10 Bonacina, Maria Paola 10 Weller, Daniel S. 7 Schmidt, Renate A. 6 de Nivelle, Hans 6 Pichler, Reinhard 5 Cerna, David M. 5 Egly, Uwe 5 Gottlob, Georg 5 Hustadt, Ullrich 5 Reis, Giselle 5 Weidenbach, Christoph 5 Woltzenlogel Paleo, Bruno 5 Zach, Richard 4 de Moura, Leonardo 4 Fontaine, Pascal 4 Lolic, Anela 4 Motik, Boris 4 Voronkov, Andrei 4 Xu, Yang 3 Buss, Samuel R. 3 Eberhard, Sebastian 3 Ebner, Gabriel 3 Echenim, Mnacho 3 Fermüller, Christian G. 3 Liu, Jun 3 Lynch, Christopher A. 3 Moser, Georg 3 Tammet, Tanel 3 Wernhard, Christoph 3 Wolfsteiner, Simon 2 Afshari, Bahareh 2 Aguilera, Juan Pablo 2 Alonderis, Romas 2 Avron, Arnon 2 Baumgartner, Peter 2 Beckmann, Arnold 2 Bjørner, Nikolaj S. 2 Bromberger, Martin 2 Caferra, Ricardo 2 Caleiro, Carlos 2 Chen, Shuwei 2 Fietzke, Arnaud 2 Goubault-Larrecq, Jean 2 Hähnle, Reiner 2 He, Xingxing 2 Leigh, Graham Emil 2 Libal, Tomer 2 Limet, Sébastien 2 Lisitsa, Alexei P. 2 Marcos, João 2 Nguyen, Linh Anh 2 Preining, Norbert 2 Ruan, Da 2 Salzer, Gernot 2 Sattler, Ulrike 2 Schlichtkrull, Anders 2 Straßburger, Lutz 2 Verma, Kumar Neeraj 2 Volpe, Marco 2 Winkler, Sarah 2 Wirth, Claus-Peter 2 Woltran, Stefan 2 Zamansky, Anna 1 Affeldt, Reynald 1 Areces, Carlos 1 Armando, Alessandro 1 Aschieri, Federico 1 Audemard, Gilles 1 Autexier, Serge 1 Bachmair, Leo 1 Barbosa, Haniel 1 Benhamou, Belaid 1 Benzmüller, Christoph Ewald 1 Bibel, Wolfgang 1 Blanchette, Jasmin Christian 1 Bourely, Christophe 1 Boy de la Tour, Thierry 1 Braüner, Torben 1 Brogi, Antonio 1 Brüning, Stefan 1 Burghardt, Jochen 1 Bydžovský, Jan 1 Carbone, Alessandra 1 Chen, Ta 1 Cho, Jung Wan 1 Ciabattoni, Agata 1 Comon-Lundh, Hubert 1 De Oliveira, Diego Caminha B. 1 de Rijke, Maarten 1 Degtyarev, Anatoli Ivanovich 1 Déharbe, David 1 Demri, Stéphane P. 1 Dershowitz, Nachum 1 Dixon, Clare 1 Dunchev, Cvetan 1 Dunchev, Tsvetan ...and 103 more Authors all top 5 Cited in 33 Serials 27 Journal of Automated Reasoning 19 Annals of Pure and Applied Logic 15 Theoretical Computer Science 14 Journal of Symbolic Computation 10 Information and Computation 6 The Journal of Symbolic Logic 5 Artificial Intelligence 4 Studia Logica 4 MSCS. Mathematical Structures in Computer Science 4 Annals of Mathematics and Artificial Intelligence 3 Information Sciences 3 Archive for Mathematical Logic 3 The Review of Symbolic Logic 2 Information Processing Letters 2 Soft Computing 2 Journal of Applied Logic 1 Computers & Mathematics with Applications 1 Lithuanian Mathematical Journal 1 Applied Mathematics and Computation 1 Notre Dame Journal of Formal Logic 1 Bulletin of the Section of Logic 1 Science of Computer Programming 1 Order 1 International Journal of Foundations of Computer Science 1 Journal of Applied Non-Classical Logics 1 The Bulletin of Symbolic Logic 1 Constraints 1 Mathematical Problems in Engineering 1 The Journal of Logic and Algebraic Programming 1 Mathematics in Computer Science 1 Logica Universalis 1 Logical Methods in Computer Science 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 12 Fields 149 Mathematical logic and foundations (03-XX) 135 Computer science (68-XX) 3 Information and communication theory, circuits (94-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 Quantum theory (81-XX) 1 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Group theory and generalizations (20-XX) 1 Manifolds and cell complexes (57-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year