Alexander Leitsch

Orcid: 0000-0002-7084-7878

Affiliations:
  • TU Wien, Vienna, Autria


According to our database1, Alexander Leitsch authored at least 69 papers between 1980 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
On Proof Schemata and Primitive Recursive Arithmetic.
Proceedings of the LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024, 2024

Herbrand's Theorem in Inductive Proofs.
Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

2021
Schematic Refutations of Formula Schemata.
J. Autom. Reason., 2021

2020
An abstract form of the first epsilon theorem.
J. Log. Comput., 2020

On the Unification of Term Schemata.
Proceedings of the 34th International Workshop on Unification, 2020

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

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

2018
The problem of Π<sub>2</sub>-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

2017
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. Log., 2017

2016
The problem of Pi_2-cut-introduction.
CoRR, 2016

Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version].
CoRR, 2016

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

2015
Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper].
CoRR, 2015

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

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

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

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

2013
CERES for First-Order Schemata
CoRR, 2013

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

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

System Feature Description: Importing Refutations into the GAPT Framework.
Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 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

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

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

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

2008
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.
Math. Struct. Comput. Sci., 2008

How to Acknowledge Hypercomputation?
Complex Syst., 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

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

Event-Related Outputs of Computations in P Systems.
J. Autom. Lang. Comb., 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

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

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

2001
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

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

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

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

1998
Decision Procedures and Model Building in Equational Clause Logic.
Log. J. 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

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

1996
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

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

1994
On Skolemization and Proof Complexity.
Fundam. Informaticae, 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

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

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

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

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

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

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

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

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

1985
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

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

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


  Loading...