Alexander Leitsch

Publication Activity (10 Years)

Years Active: 1980-2021
Publications (10 Years): 16

Top Topics

Proof Theoretic

Cut Elimination

Intuitionistic Logic

Theorem Proving

Top Venues

J. Autom. Reason.

J. Log. Comput.

Publications

David M. Cerna, Alexander Leitsch, Anela Lolic
Schematic Refutations of Formula Schemata. J. Autom. Reason. 65 (5) (2021)
David M. Cerna, Alexander Leitsch, Anela Lolic
On the Unification of Term Schemata. UNIF (2020)
Matthias Baaz, Alexander Leitsch, Anela Lolic
An abstract form of the first epsilon theorem. J. Log. Comput. 30 (8) (2020)
Gabriel Ebner, Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller
On the Generation of Quantified Lemmas. J. Autom. Reason. 63 (1) (2019)
Alexander Leitsch, Anela Lolic
Extraction of Expansion Trees. J. Autom. Reason. 62 (3) (2019)
David M. Cerna, Alexander Leitsch, Anela Lolic
Schematic Refutations of Formula Schemata. CoRR (2019)
Alexander Leitsch, Michael Peter Lettmann
-cut-introduction. Theor. Comput. Sci. 706 (2018)
Matthias Baaz, Alexander Leitsch, Anela Lolic
A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. LFCS (2018)
David M. Cerna, Alexander Leitsch, Giselle Reis, Simon Wolfsteiner
Ceres in intuitionistic logic. Ann. Pure Appl. Log. 168 (10) (2017)
Alexander Leitsch, Nicolas Peltier, Daniel Weller
CERES for first-order schemata. J. Log. Comput. 27 (7) (2017)
Matthias Baaz, Alexander Leitsch
On the Complexity of Translations from Classical to Intuitionistic Proofs. FLAP 4 (4) (2017)
Alexander Leitsch, Michael Peter Lettmann
The problem of Pi_2-cut-introduction. CoRR (2016)
David M. Cerna, Alexander Leitsch
Schematic Cut Elimination and the Ordered Pigeonhole Principle. IJCAR (2016)
David M. Cerna, Alexander Leitsch
Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]. CoRR (2016)
David M. Cerna, Alexander Leitsch
Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]. CoRR (2015)
Matthias Baaz, Alexander Leitsch, Giselle Reis
A Note on the Complexity of Classical and Intuitionistic Proofs. LICS (2015)
Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller
Introducing Quantified Cuts in Logic with Equality. IJCAR (2014)
Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller
Introducing Quantified Cuts in Logic with Equality. CoRR (2014)
Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller
Algorithmic introduction of quantified cuts. Theor. Comput. Sci. 549 (2014)
Matthias Baaz, Alexander Leitsch
Cut-Elimination: Syntax and Semantics. Stud Logica 102 (6) (2014)
Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller
Algorithmic Introduction of Quantified Cuts. CoRR (2014)
Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia, Daniel Weller
CERES for First-Order Schemata CoRR (2013)
Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia, Daniel Weller
Cut-Elimination and Proof Schemata. TbiLLC (2013)
Stefan Hetzl, Alexander Leitsch, Daniel Weller
Towards Algorithmic Cut-Introduction. LPAR (2012)
Alexander Leitsch, Giselle Reis, Bruno Woltzenlogel Paleo
Towards CERes in intuitionistic logic. CSL (2012)
Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel Paleo
System Feature Description: Importing Refutations into the GAPT Framework. PxTP (2012)
Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel Paleo
PROOFTOOL: a GUI for the GAPT Framework. UITP (2012)
Alexander Leitsch, Tomer Libal
A Resolution Calculus for Second-order Logic with Eager Unification. PAAR@IJCAR (2012)
Stefan Hetzl, Alexander Leitsch, Daniel Weller
CERES in higher-order logic. Ann. Pure Appl. Log. 162 (12) (2011)
Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo
System Description: The Proof Transformation System CERES. IJCAR (2010)
Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo
A Clausal Approach to Proof Analysis in Second-Order Logic. LFCS (2009)
Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo
Transforming and Analyzing Proofs in the CERES-System. LPAR Workshops (2008)
Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr
CERES: An analysis of Fürstenberg's proof of the infinity of primes. Theor. Comput. Sci. 403 (2-3) (2008)
Alexander Leitsch, Günter Schachner, Karl Svozil
How to Acknowledge Hypercomputation? Complex Syst. 18 (1) (2008)
Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo
Herbrand Sequent Extraction. AISC/MKM/Calculemus (2008)
Agata Ciabattoni, Alexander Leitsch
Towards an algorithmic construction of cut-elimination procedures. Math. Struct. Comput. Sci. 18 (1) (2008)
Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr
Proof Transformation by CERES. MKM (2006)
Matteo Cavaliere, Rudolf Freund, Alexander Leitsch, Gheorghe Paun
Event-Related Outputs of Computations in P Systems. J. Autom. Lang. Comb. 11 (3) (2006)
Stefan Hetzl, Alexander Leitsch
Proof Transformations and Structural Invariance. Algebraic and Proof-theoretic Aspects of Non-classical Logics (2006)
Matthias Baaz, Alexander Leitsch
Towards a clausal analysis of cut-elimination. J. Symb. Comput. 41 (3-4) (2006)
Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr
Cut-Elimination: Experiments with CERES. LPAR (2004)
Matthias Baaz, Alexander Leitsch
CERES in Many-Valued Logics. LPAR (2004)
Matthias Baaz, Alexander Leitsch
Comparing the Complexity of Cut-Elimination Methods. Proof Theory in Computer Science (2001)
Matthias Baaz, Alexander Leitsch
Cut-elimination and Redundancy-elimination by Resolution. J. Symb. Comput. 29 (2) (2000)
Matthias Baaz, Alexander Leitsch
Cut Normal Forms and Proof Complexity. Ann. Pure Appl. Log. 97 (1-3) (1999)
Matthias Baaz, Alexander Leitsch, Georg Moser
System Description: CutRes 0.1: Cut Elimination by Resolution. CADE (1999)
Alexander Leitsch
Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction. FTP (LNCS Selection) (1998)
Christian G. Fermüller, Alexander Leitsch
Decision Procedures and Model Building in Equational Clause Logic. Log. J. IGPL 6 (1) (1998)
Matthias Baaz, Alexander Leitsch, Richard Zach
Completeness of a First-Order Temporal Logic with Time-Gaps. Theor. Comput. Sci. 160 (1&2) (1996)
Christian G. Fermüller, Alexander Leitsch
Hyperresolution and Automated Model Building. J. Log. Comput. 6 (2) (1996)
Matthias Baaz, Alexander Leitsch
Fast Cut-Elimination by Projection. CSL (1996)
Matthias Baaz, Alexander Leitsch, Richard Zach
Incompleteness of a First-Order Gödel Logic and Some Temporal Logics of Programs. CSL (1995)
Matthias Baaz, Alexander Leitsch
On Skolemization and Proof Complexity. Fundam. Informaticae 20 (4) (1994)
Matthias Baaz, Christian G. Fermüller, Alexander Leitsch
A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation LICS (1994)
Alexander Leitsch
Deciding Clause Classes by Semantic Clash Resolution. Fundam. Informaticae 18 (1993)
Christian G. Fermüller, Alexander Leitsch
Model Building by Resolution. CSL (1992)
Matthias Baaz, Alexander Leitsch
Complexity of Resolution Proofs and Function Introduction. Ann. Pure Appl. Log. 57 (3) (1992)
Matthias Baaz, Alexander Leitsch
A Strong Problem Reduction Method Based on Function Introduction. ISSAC (1990)
Alexander Leitsch
Deciding Horn Classes by Hyperresolution. CSL (1989)
Alexander Leitsch
On Different Concepts of Resolution. Math. Log. Q. 35 (1) (1989)
Matthias Baaz, Alexander Leitsch
Strong splitting rules in automated theorem proving. EUROCAL (1987)
Matthias Baaz, Alexander Leitsch
Eine Methode zur automatischen Problemreduktion. ÖGAI (1985)
Georg Gottlob, Alexander Leitsch
On the Efficiency of Subsumption Algorithms J. ACM 32 (2) (1985)
Georg Gottlob, Alexander Leitsch
Fast Subsumption Algorithms. European Conference on Computer Algebra (2) (1985)
Alexander Leitsch
Fiducial intervals for the waiting time in batch and time-sharing systems. Computing 28 (4) (1982)
Alexander Leitsch
Complexity of index sets and translating functions. Fundam. Informaticae 3 (2) (1980)