×

zbMATH — the first resource for mathematics

Leitsch, Alexander

Compute Distance To:
Author ID: leitsch.alexander Recent zbMATH articles by "Leitsch, Alexander"
Published as: Leitsch, A.; Leitsch, Alexander
Documents Indexed: 74 Publications since 1978, including 7 Books
Reviewing Activity: 39 Reviews

Publications by Year

Citations contained in zbMATH Open

51 Publications have been cited 353 times in 171 Documents Cited by Year
The resolution calculus. Zbl 0867.68095
Leitsch, Alexander
29
1997
Resolution decision procedures. Zbl 0993.68119
Fermüller, Christian G.; Leitsch, Alexander; Hustadt, Ullrich; Tammet, Tanel
28
2001
On Skolemization and proof complexity. Zbl 0815.03003
Baaz, Matthias; Leitsch, Alexander
24
1994
Cut-elimination and redundancy-elimination by resolution. Zbl 0976.03059
Baaz, Matthias; Leitsch, Alexander
20
2000
Hyperresolution and automated model building. Zbl 0861.68086
Fermüller, Christian; Leitsch, Alexander
20
1996
Resolution methods for the decision problem. Zbl 0789.03013
Fermüller, C. (ed.); Leitsch, A. (ed.); Tammet, Tanel (ed.); Zamov, Nail (ed.)
17
1993
Automated model building. Zbl 1085.03009
Caferra, Ricardo; Leitsch, Alexander; Peltier, Nicholas
14
2004
Cut normal forms and proof complexity. Zbl 0940.03062
Baaz, Matthias; Leitsch, Alexander
14
1999
Normal form transformations. Zbl 1005.03013
Baaz, Matthias; Egly, Uwe; Leitsch, Alexander
13
2001
On the efficiency of subsumption algorithms. Zbl 0633.68028
Gottlob, G.; Leitsch, A.
13
1985
Algorithmic introduction of quantified cuts. Zbl 1393.03050
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
11
2014
Towards algorithmic cut-introduction. Zbl 1352.68213
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel
10
2012
Decision procedures and model building in equational clause logic. Zbl 0903.03010
Fermüller, Christian G.; Leitsch, Alexander
10
1998
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
9
2008
Cut-elimination: experiments with CERES. Zbl 1108.03305
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik
9
2005
Herbrand sequent extraction. Zbl 1166.68347
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno
8
2008
Deciding clause classes by semantic clash resolution. Zbl 0789.03016
Leitsch, Alexander
8
1993
Introducing quantified cuts in logic with equality. Zbl 1423.68418
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel
7
2014
Methods of cut-elimination. Zbl 1225.03075
Baaz, Matthias; Leitsch, Alexander
7
2011
Towards a clausal analysis of cut-elimination. Zbl 1125.03013
Baaz, Matthias; Leitsch, Alexander
7
2006
Completeness of a first-order temporal logic with time-gaps. Zbl 0872.68171
Baaz, Matthias; Leitsch, Alexander; Zach, Richard
7
1996
On different concepts of resolution. Zbl 0646.03011
Leitsch, Alexander
6
1989
Proof transformation by CERES. Zbl 1125.03012
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik
5
2006
Complexity of resolution proofs and function introduction. Zbl 0769.03009
Baaz, Matthias; Leitsch, Alexander
5
1992
CERES in higher-order logic. Zbl 1259.03071
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel
4
2011
Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Zbl 0968.00052
Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.)
4
2001
Fast subsumption algorithms. Zbl 0588.68044
Gottlob, G.; Leitsch, A.
4
1985
Cut-elimination and proof schemata. Zbl 1326.03069
Dunchev, Cvetan; Leitsch, Alexander; Rukhaia, Mikheil; Weller, Daniel
3
2015
CERES in many-valued logics. Zbl 1109.03007
Baaz, Matthias; Leitsch, Alexander
3
2005
Model building by resolution. Zbl 0788.68128
Fermüller, Christian G.; Leitsch, Alexander
3
1993
Decision-algorithms for the associativity of Latin squares. Zbl 0509.05022
Leitsch, A.
3
1983
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
Towards an algorithmic construction of cut-elimination procedures. Zbl 1138.03043
Ciabattoni, Agata; Leitsch, Alexander
2
2008
Proof transformations and structural invariance. Zbl 1123.03050
Hetzl, Stefan; Leitsch, Alexander
2
2007
Decision procedures and model building or how to improve logical information in automated deduction. Zbl 0966.03011
Leitsch, Alexander
2
2000
Fast cut-elimination by projection. Zbl 0889.03048
Baaz, Matthias; Leitsch, Alexander
2
1997
Methods of functional extension. Zbl 0840.03042
Baaz, Matthias; Leitsch, Alexander
2
1995
Deciding Horn classes by hyperresolution. Zbl 0925.03056
Leitsch, Alexander
2
1990
On the generation of quantified lemmas. Zbl 1459.03011
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
1
2019
Schematic cut elimination and the ordered pigeonhole principle. Zbl 06623265
Cerna, David M.; Leitsch, Alexander
1
2016
Towards CERes in intuitionistic logic. Zbl 1252.03124
Leitsch, Alexander; Reis, Giselle; Woltzenlogel Paleo, Bruno
1
2012
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
1
2009
Comparing the complexity of cut-elimination methods. Zbl 1024.03058
Baaz, Matthias; Leitsch, Alexander
1
2001
Strong splitting rules in automated theorem proving. Zbl 1209.68503
Baaz, Matthias; Leitsch, Alexander
1
1989
Implication algorithms for classes of Horn clauses. Zbl 0679.68172
Leitsch, A.
1
1989
On some formal problems in resolution theorem proving. Zbl 0689.03004
Leitsch, Alexander
1
1988
Eine Methode zur automatischen Problemreduktion. Zbl 0607.68071
Baaz, M.; Leitsch, A.
1
1985
Die Anwendung starker Reduktionsregeln in automatischen Beweisen. Zbl 0596.03007
Baaz, Matthias; Leitsch, Alexander
1
1985
On the generation of quantified lemmas. Zbl 1459.03011
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
1
2019
The problem of \(\Pi_{2}\)-cut-introduction. Zbl 1423.03240
Leitsch, Alexander; Lettmann, Michael
2
2018
Schematic cut elimination and the ordered pigeonhole principle. Zbl 06623265
Cerna, David M.; Leitsch, Alexander
1
2016
Cut-elimination and proof schemata. Zbl 1326.03069
Dunchev, Cvetan; Leitsch, Alexander; Rukhaia, Mikheil; Weller, Daniel
3
2015
Algorithmic introduction of quantified cuts. Zbl 1393.03050
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
11
2014
Introducing quantified cuts in logic with equality. Zbl 1423.68418
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel
7
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
10
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
7
2011
CERES in higher-order logic. Zbl 1259.03071
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel
4
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
1
2009
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
9
2008
Herbrand sequent extraction. Zbl 1166.68347
Hetzl, Stefan; Leitsch, Alexander; Weller, Daniel; Woltzenlogel Paleo, Bruno
8
2008
Towards an algorithmic construction of cut-elimination procedures. Zbl 1138.03043
Ciabattoni, Agata; Leitsch, Alexander
2
2008
Proof transformations and structural invariance. Zbl 1123.03050
Hetzl, Stefan; Leitsch, Alexander
2
2007
Towards a clausal analysis of cut-elimination. Zbl 1125.03013
Baaz, Matthias; Leitsch, Alexander
7
2006
Proof transformation by CERES. Zbl 1125.03012
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik
5
2006
Cut-elimination: experiments with CERES. Zbl 1108.03305
Baaz, Matthias; Hetzl, Stefan; Leitsch, Alexander; Richter, Clemens; Spohr, Hendrik
9
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
14
2004
Resolution decision procedures. Zbl 0993.68119
Fermüller, Christian G.; Leitsch, Alexander; Hustadt, Ullrich; Tammet, Tanel
28
2001
Normal form transformations. Zbl 1005.03013
Baaz, Matthias; Egly, Uwe; Leitsch, Alexander
13
2001
Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Zbl 0968.00052
Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.)
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
20
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
14
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
29
1997
Fast cut-elimination by projection. Zbl 0889.03048
Baaz, Matthias; Leitsch, Alexander
2
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
7
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
24
1994
Resolution methods for the decision problem. Zbl 0789.03013
Fermüller, C. (ed.); Leitsch, A. (ed.); Tammet, Tanel (ed.); Zamov, Nail (ed.)
17
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
3
1993
Complexity of resolution proofs and function introduction. Zbl 0769.03009
Baaz, Matthias; Leitsch, Alexander
5
1992
Deciding Horn classes by hyperresolution. Zbl 0925.03056
Leitsch, Alexander
2
1990
On different concepts of resolution. Zbl 0646.03011
Leitsch, Alexander
6
1989
Strong splitting rules in automated theorem proving. Zbl 1209.68503
Baaz, Matthias; Leitsch, Alexander
1
1989
Implication algorithms for classes of Horn clauses. Zbl 0679.68172
Leitsch, A.
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.
13
1985
Fast subsumption algorithms. Zbl 0588.68044
Gottlob, G.; Leitsch, A.
4
1985
Eine Methode zur automatischen Problemreduktion. Zbl 0607.68071
Baaz, M.; Leitsch, A.
1
1985
Die Anwendung starker Reduktionsregeln in automatischen Beweisen. Zbl 0596.03007
Baaz, Matthias; Leitsch, Alexander
1
1985
Decision-algorithms for the associativity of Latin squares. Zbl 0509.05022
Leitsch, A.
3
1983
all top 5

Cited by 175 Authors

16 Baaz, Matthias
16 Hetzl, Stefan
16 Leitsch, Alexander
12 Peltier, Nicolas
7 Bonacina, Maria Paola
7 Weller, Daniel S.
6 de Nivelle, Hans
6 Pichler, Reinhard
6 Woltzenlogel Paleo, Bruno
5 Egly, Uwe
5 Gottlob, Georg
5 Hustadt, Ullrich
5 Reis, Giselle
5 Schmidt, Renate A.
4 Cerna, David M.
4 Lynch, Christopher A.
4 Motik, Boris
4 Voronkov, Andrei
4 Weidenbach, Christoph
4 Xu, Yang
3 de Moura, Leonardo
3 Echenim, Mnacho
3 Fermüller, Christian G.
3 Fontaine, Pascal
3 Liu, Jun
3 Wolfsteiner, Simon
3 Zach, Richard
2 Alonderis, Romas
2 Avron, Arnon
2 Baumgartner, Peter
2 Beckmann, Arnold
2 Buss, Samuel R.
2 Caferra, Ricardo
2 Caleiro, Carlos
2 Chen, Shuwei
2 Eberhard, Sebastian
2 Ebner, Gabriel
2 Fietzke, Arnaud
2 Goubault-Larrecq, Jean
2 Hájek, Petr
2 Limet, Sébastien
2 Lisitsa, Alexei
2 Marcos, João
2 Moser, Georg
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 Woltran, Stefan
2 Zamansky, Anna
1 Affeldt, Reynald
1 Afshari, Bahareh
1 Aguilera, Juan Pablo
1 Areces, Carlos
1 Armando, Alessandro
1 Aschieri, Federico
1 Audemard, Gilles
1 Autexier, Serge
1 Barbosa, Haniel
1 Benhamou, Belaid
1 Benzmüller, Christoph Ewald
1 Bjørner, Nikolaj S.
1 Blanchette, Jasmin Christian
1 Bourely, Christophe
1 Brogi, Antonio
1 Bromberger, Martin
1 Buss, Sam
1 Carbone, Alessandra
1 Carbone, Antonio
1 Cho, Jung Wan
1 Ciabattoni, Agata
1 Cintula, Petr
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 Eisinger, Norbert
1 Fish, Andrew
1 Fisher, Michael E.
1 Fleury, Mathias
1 Formisano, Andrea
1 Friedrich, Gerhard E.
1 Fu, Jun
1 Geisler, Tim
1 Georgieva, Lilia
1 Giedra, Haroldas
1 Gladisch, Christoph D.
1 Goldstern, Martin Robert
1 Goré, Rajeev Prabhakar
1 Gorín, Daniel
1 Gorzny, Jan
1 Gratzl, Norbert
...and 75 more Authors

Citations by Year