×
Author ID: leitsch.alexander Recent zbMATH articles by "Leitsch, Alexander"
Published as: Leitsch, Alexander; Leitsch, A.

Publications by Year

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

Citations by Year