Alexander Leitsch

78 papers A* 2A 5B 10Misc 2Journal 36Unranked 16

Year	Rank	Type	Title / Venue / Authors
2026	—	`book`	First-Order Schemata and Inductive Proof Analysis, 1 Alexander Leitsch, David Michael Cerna, Anela Lolic
2025	J	`jnl`	Extracting Herbrand systems from refutation schemata. J. Log. Comput. Alexander Leitsch, Anela Lolic
2024	B	`conf`	Herbrand's Theorem in Inductive Proofs. LPAR Alexander Leitsch, Anela Lolic
2024	—	`conf`	On Proof Schemata and Primitive Recursive Arithmetic. LPAR Complementary Volume Alexander Leitsch, Anela Lolic, Stella Mahler
2024	—	`conf`	Towards an Analysis of Proofs in Arithmetic. LSFA Alexander Leitsch, Anela Lolic, Stella Mahler
2021	J	`jnl`	Schematic Refutations of Formula Schemata. J. Autom. Reason. David M. Cerna, Alexander Leitsch, Anela Lolic
2020	J	`jnl`	An abstract form of the first epsilon theorem. J. Log. Comput. Matthias Baaz, Alexander Leitsch, Anela Lolic
2020	—	`conf`	On the Unification of Term Schemata. UNIF David M. Cerna, Alexander Leitsch, Anela Lolic
2019	J	`jnl`	Extraction of Expansion Trees. J. Autom. Reason. Alexander Leitsch, Anela Lolic
2019	J	`jnl`	On the Generation of Quantified Lemmas. J. Autom. Reason. Gabriel Ebner, Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller
2019	J	`jnl`	Schematic Refutations of Formula Schemata. CoRR David M. Cerna, Alexander Leitsch, Anela Lolic
2018	Misc	`conf`	A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. LFCS Matthias Baaz, Alexander Leitsch, Anela Lolic
2018	J	`jnl`	The problem of Π Theor. Comput. Sci. Alexander Leitsch, Michael Peter Lettmann
2017	J	`jnl`	CERES for first-order schemata. J. Log. Comput. Alexander Leitsch, Nicolas Peltier, Daniel Weller
2017	J	`jnl`	Ceres in intuitionistic logic. Ann. Pure Appl. Log. David M. Cerna, Alexander Leitsch, Giselle Reis, Simon Wolfsteiner
2017	J	`jnl`	On the Complexity of Translations from Classical to Intuitionistic Proofs. FLAP Matthias Baaz, Alexander Leitsch
2016	A	`conf`	Schematic Cut Elimination and the Ordered Pigeonhole Principle. IJCAR David M. Cerna, Alexander Leitsch
2016	J	`jnl`	Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]. CoRR David M. Cerna, Alexander Leitsch
2016	J	`jnl`	The problem of Pi_2-cut-introduction. CoRR Alexander Leitsch, Michael Peter Lettmann
2015	A*	`conf`	A Note on the Complexity of Classical and Intuitionistic Proofs. LICS Matthias Baaz, Alexander Leitsch, Giselle Reis
2015	J	`jnl`	Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]. CoRR David M. Cerna, Alexander Leitsch
2014	J	`jnl`	Algorithmic Introduction of Quantified Cuts. CoRR Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller
2014	J	`jnl`	Algorithmic introduction of quantified cuts. Theor. Comput. Sci. Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller
2014	J	`jnl`	Cut-Elimination: Syntax and Semantics. Stud Logica Matthias Baaz, Alexander Leitsch
2014	A	`conf`	Introducing Quantified Cuts in Logic with Equality. IJCAR Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller
2014	J	`jnl`	Introducing Quantified Cuts in Logic with Equality. CoRR Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller
2013	J	`jnl`	CERES for First-Order Schemata CoRR Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia, Daniel Weller
2013	—	`conf`	Cut-Elimination and Proof Schemata. TbiLLC Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia, Daniel Weller
2012	—	`conf`	A Resolution Calculus for Second-order Logic with Eager Unification. PAAR@IJCAR Alexander Leitsch, Tomer Libal
2012	—	`conf`	PROOFTOOL: a GUI for the GAPT Framework. UITP Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel Paleo
2012	—	`conf`	System Feature Description: Importing Refutations into the GAPT Framework. PxTP Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel Paleo
2012	B	`conf`	Towards Algorithmic Cut-Introduction. LPAR Stefan Hetzl, Alexander Leitsch, Daniel Weller
2012	B	`conf`	Towards CERes in intuitionistic logic. CSL Alexander Leitsch, Giselle Reis, Bruno Woltzenlogel Paleo
2011	J	`jnl`	CERES in higher-order logic. Ann. Pure Appl. Log. Stefan Hetzl, Alexander Leitsch, Daniel Weller
2010	A	`conf`	System Description: The Proof Transformation System CERES. IJCAR Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo
2009	Misc	`conf`	A Clausal Approach to Proof Analysis in Second-Order Logic. LFCS Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo
2008	J	`jnl`	CERES: An analysis of Fürstenberg's proof of the infinity of primes. Theor. Comput. Sci. Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr
2008	—	`conf`	Herbrand Sequent Extraction. AISC/MKM/Calculemus Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo
2008	J	`jnl`	How to Acknowledge Hypercomputation? Complex Syst. Alexander Leitsch, Günter Schachner, Karl Svozil
2008	J	`jnl`	Towards an algorithmic construction of cut-elimination procedures. Math. Struct. Comput. Sci. Agata Ciabattoni, Alexander Leitsch
2008	—	`conf`	Transforming and Analyzing Proofs in the CERES-System. LPAR Workshops Stefan Hetzl, Alexander Leitsch, Daniel Weller, Bruno Woltzenlogel Paleo
2006	J	`jnl`	Event-Related Outputs of Computations in P Systems. J. Autom. Lang. Comb. Matteo Cavaliere, Rudolf Freund, Alexander Leitsch, Gheorghe Paun
2006	—	`conf`	Proof Transformation by CERES. MKM Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr
2006	—	`conf`	Proof Transformations and Structural Invariance. Algebraic and Proof-theoretic Aspects of Non-classical Logics Stefan Hetzl, Alexander Leitsch
2006	J	`jnl`	Towards a clausal analysis of cut-elimination. J. Symb. Comput. Matthias Baaz, Alexander Leitsch
2004	B	`conf`	CERES in Many-Valued Logics. LPAR Matthias Baaz, Alexander Leitsch
2004	B	`conf`	Cut-Elimination: Experiments with CERES. LPAR Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr
2001	A	`ed.`	Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings IJCAR Rajeev Goré, Alexander Leitsch, Tobias Nipkow
2001	—	`conf`	Comparing the Complexity of Cut-Elimination Methods. Proof Theory in Computer Science Matthias Baaz, Alexander Leitsch
2001	—	`ch.`	Normal Form Transformations. Handbook of Automated Reasoning Matthias Baaz, Uwe Egly, Alexander Leitsch
2001	—	`ch.`	Resolution Decision Procedures. Handbook of Automated Reasoning Christian G. Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet
2000	J	`jnl`	Cut-elimination and Redundancy-elimination by Resolution. J. Symb. Comput. Matthias Baaz, Alexander Leitsch
1999	J	`jnl`	Cut Normal Forms and Proof Complexity. Ann. Pure Appl. Log. Matthias Baaz, Alexander Leitsch
1999	A	`conf`	System Description: CutRes 0.1: Cut Elimination by Resolution. CADE Matthias Baaz, Alexander Leitsch, Georg Moser
1998	J	`jnl`	Decision Procedures and Model Building in Equational Clause Logic. Log. J. IGPL Christian G. Fermüller, Alexander Leitsch
1998	—	`conf`	Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction. FTP (LNCS Selection) Alexander Leitsch
1997	—	`ed.`	Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, KGC'97, Vienna, Austria, August 25-29, 1997, Proceedings Kurt Gödel Colloquium Georg Gottlob, Alexander Leitsch, Daniele Mundici
1997	—	`book`	The Resolution Calculus. Alexander Leitsch
1996	J	`jnl`	Completeness of a First-Order Temporal Logic with Time-Gaps. Theor. Comput. Sci. Matthias Baaz, Alexander Leitsch, Richard Zach
1996	B	`conf`	Fast Cut-Elimination by Projection. CSL Matthias Baaz, Alexander Leitsch
1996	J	`jnl`	Hyperresolution and Automated Model Building. J. Log. Comput. Christian G. Fermüller, Alexander Leitsch
1995	B	`conf`	Incompleteness of a First-Order Gödel Logic and Some Temporal Logics of Programs. CSL Matthias Baaz, Alexander Leitsch, Richard Zach
1994	A*	`conf`	A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation LICS Matthias Baaz, Christian G. Fermüller, Alexander Leitsch
1994	J	`jnl`	On Skolemization and Proof Complexity. Fundam. Informaticae Matthias Baaz, Alexander Leitsch
1993	—	`ed.`	Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, Proceedings Kurt Gödel Colloquium Georg Gottlob, Alexander Leitsch, Daniele Mundici
1993	J	`jnl`	Deciding Clause Classes by Semantic Clash Resolution. Fundam. Informaticae Alexander Leitsch
1993	—	`book`	Resolution Methods for the Decision Problem Christian G. Fermüller, Alexander Leitsch, Tanel Tammet, N. K. Zamov
1992	J	`jnl`	Complexity of Resolution Proofs and Function Introduction. Ann. Pure Appl. Log. Matthias Baaz, Alexander Leitsch
1992	B	`conf`	Model Building by Resolution. CSL Christian G. Fermüller, Alexander Leitsch
1990	B	`conf`	A Strong Problem Reduction Method Based on Function Introduction. ISSAC Matthias Baaz, Alexander Leitsch
1989	B	`conf`	Deciding Horn Classes by Hyperresolution. CSL Alexander Leitsch
1989	J	`jnl`	On Different Concepts of Resolution. Math. Log. Q. Alexander Leitsch
1987	—	`conf`	Strong splitting rules in automated theorem proving. EUROCAL Matthias Baaz, Alexander Leitsch
1985	—	`conf`	Eine Methode zur automatischen Problemreduktion. ÖGAI Matthias Baaz, Alexander Leitsch
1985	—	`conf`	Fast Subsumption Algorithms. European Conference on Computer Algebra (2) Georg Gottlob, Alexander Leitsch
1985	J	`jnl`	On the Efficiency of Subsumption Algorithms J. ACM Georg Gottlob, Alexander Leitsch
1982	J	`jnl`	Fiducial intervals for the waiting time in batch and time-sharing systems. Computing Alexander Leitsch
1980	J	`jnl`	Complexity of index sets and translating functions. Fundam. Informaticae Alexander Leitsch