Alexander Leitsch

According to our database1, Alexander Leitsch authored at least 59 papers between 1980 and 2019.

Collaborative distances:



In proceedings 
PhD thesis 





Extraction of Expansion Trees.
J. Autom. Reasoning, 2019

On the Generation of Quantified Lemmas.
J. Autom. Reasoning, 2019

The problem of Π2-cut-introduction.
Theor. Comput. Sci., 2018

A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem.
Proceedings of the Logical Foundations of Computer Science - International Symposium, 2018

CERES for first-order schemata.
J. Log. Comput., 2017

On the Complexity of Translations from Classical to Intuitionistic Proofs.
FLAP, 2017

Ceres in intuitionistic logic.
Ann. Pure Appl. Logic, 2017

Schematic Cut Elimination and the Ordered Pigeonhole Principle.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

A Note on the Complexity of Classical and Intuitionistic Proofs.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Algorithmic introduction of quantified cuts.
Theor. Comput. Sci., 2014

Cut-Elimination: Syntax and Semantics.
Studia Logica, 2014

Introducing Quantified Cuts in Logic with Equality.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

Cut-Elimination and Proof Schemata.
Proceedings of the Logic, Language, and Computation, 2013

PROOFTOOL: a GUI for the GAPT Framework.
Proceedings of the Proceedings 10th International Workshop On User Interfaces for Theorem Provers, 2012

Towards Algorithmic Cut-Introduction.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Towards CERes in intuitionistic logic.
Proceedings of the Computer Science Logic (CSL'12), 2012

A Resolution Calculus for Second-order Logic with Eager Unification.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

CERES in higher-order logic.
Ann. Pure Appl. Logic, 2011

System Description: The Proof Transformation System CERES.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

A Clausal Approach to Proof Analysis in Second-Order Logic.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2009

CERES: An analysis of Fürstenberg's proof of the infinity of primes.
Theor. Comput. Sci., 2008

Towards an algorithmic construction of cut-elimination procedures.
Mathematical Structures in Computer Science, 2008

How to Acknowledge Hypercomputation?
Complex Systems, 2008

Transforming and Analyzing Proofs in the CERES-System.
Proceedings of the LPAR 2008 Workshops, 2008

Herbrand Sequent Extraction.
Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

Towards a clausal analysis of cut-elimination.
J. Symb. Comput., 2006

Event-Related Outputs of Computations in P Systems.
Journal of Automata, Languages and Combinatorics, 2006

Proof Transformation by CERES.
Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

Proof Transformations and Structural Invariance.
Proceedings of the Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006

CERES in Many-Valued Logics.
Proceedings of the Logic for Programming, 2004

Cut-Elimination: Experiments with CERES.
Proceedings of the Logic for Programming, 2004

Comparing the Complexity of Cut-Elimination Methods.
Proceedings of the Proof Theory in Computer Science, International Seminar, 2001

Resolution Decision Procedures.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Normal Form Transformations.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Cut-elimination and Redundancy-elimination by Resolution.
J. Symb. Comput., 2000

Cut Normal Forms and Proof Complexity.
Ann. Pure Appl. Logic, 1999

System Description: CutRes 0.1: Cut Elimination by Resolution.
Proceedings of the Automated Deduction, 1999

Decision Procedures and Model Building in Equational Clause Logic.
Logic Journal of the IGPL, 1998

Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction.
Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

The Resolution Calculus.
Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-642-60605-2, 1997

Completeness of a First-Order Temporal Logic with Time-Gaps.
Theor. Comput. Sci., 1996

Hyperresolution and Automated Model Building.
J. Log. Comput., 1996

Fast Cut-Elimination by Projection.
Proceedings of the Computer Science Logic, 10th International Workshop, 1996

Incompleteness of a First-Order Gödel Logic and Some Temporal Logics of Programs.
Proceedings of the Computer Science Logic, 9th International Workshop, 1995

On Skolemization and Proof Complexity.
Fundam. Inform., 1994

A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Deciding Clause Classes by Semantic Clash Resolution.
Fundam. Inform., 1993

Resolution Methods for the Decision Problem
Lecture Notes in Computer Science 679, Springer, ISBN: 3-540-56732-1, 1993

Complexity of Resolution Proofs and Function Introduction.
Ann. Pure Appl. Logic, 1992

Model Building by Resolution.
Proceedings of the Computer Science Logic, 6th Workshop, 1992

A Strong Problem Reduction Method Based on Function Introduction.
Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1990

On Different Concepts of Resolution.
Math. Log. Q., 1989

Deciding Horn Classes by Hyperresolution.
Proceedings of the CSL '89, 1989

Strong splitting rules in automated theorem proving.
Proceedings of the EUROCAL '87, 1987

On the Efficiency of Subsumption Algorithms
J. ACM, April, 1985

Eine Methode zur automatischen Problemreduktion.
Proceedings of the Österreichische Artificial Intelligence-Tagung, 1985

Fast Subsumption Algorithms.
Proceedings of the EUROCAL '85, 1985

Fiducial intervals for the waiting time in batch and time-sharing systems.
Computing, 1982

Complexity of index sets and translating functions.
Fundam. Inform., 1980