Alexander Leitsch

J. Autom. Reason., 2021

2020

An abstract form of the first epsilon theorem.

[BibT_eX]

[DOI]

J. Log. Comput., 2020

On the Unification of Term Schemata.

[BibT_eX]

[DOI]

Proceedings of the 34th International Workshop on Unification, 2020

2019

Extraction of Expansion Trees.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

On the Generation of Quantified Lemmas.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

2018

The problem of Π<sub>2</sub>-cut-introduction.

[BibT_eX]

[DOI]

Michael Peter Lettmann

Theor. Comput. Sci., 2018

A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science - International Symposium, 2018

2017

CERES for first-order schemata.

[BibT_eX]

[DOI]

Nicolas Peltier

J. Log. Comput., 2017

On the Complexity of Translations from Classical to Intuitionistic Proofs.

[BibT_eX]

[DOI]

FLAP, 2017

Ceres in intuitionistic logic.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2017

2016

The problem of Pi_2-cut-introduction.

[BibT_eX]

[DOI]

Michael Peter Lettmann

CoRR, 2016

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

[BibT_eX]

[DOI]

CoRR, 2016

Schematic Cut Elimination and the Ordered Pigeonhole Principle.

[BibT_eX]

[DOI]

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].

[BibT_eX]

[DOI]

CoRR, 2015

A Note on the Complexity of Classical and Intuitionistic Proofs.

[BibT_eX]

[DOI]

Giselle Reis

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014

Algorithmic introduction of quantified cuts.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2014

Cut-Elimination: Syntax and Semantics.

[BibT_eX]

[DOI]

Stud Logica, 2014

Introducing Quantified Cuts in Logic with Equality.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

CERES for First-Order Schemata

[BibT_eX]

[DOI]

CoRR, 2013

Cut-Elimination and Proof Schemata.

[BibT_eX]

[DOI]

Proceedings of the Logic, Language, and Computation, 2013

2012

PROOFTOOL: a GUI for the GAPT Framework.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 10th International Workshop On User Interfaces for Theorem Provers, 2012

System Feature Description: Importing Refutations into the GAPT Framework.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

Towards Algorithmic Cut-Introduction.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Towards CERes in intuitionistic logic.

[BibT_eX]

[DOI]

Giselle Reis

Proceedings of the Computer Science Logic (CSL'12), 2012

A Resolution Calculus for Second-order Logic with Eager Unification.

[BibT_eX]

[DOI]

Tomer Libal

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011

CERES in higher-order logic.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2011

2010

System Description: The Proof Transformation System CERES.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

A Clausal Approach to Proof Analysis in Second-Order Logic.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

Towards an algorithmic construction of cut-elimination procedures.

[BibT_eX]

[DOI]

Agata Ciabattoni

Math. Struct. Comput. Sci., 2008

How to Acknowledge Hypercomputation?

[BibT_eX]

[DOI]

Günter Schachner

Karl Svozil

Complex Syst., 2008

Transforming and Analyzing Proofs in the CERES-System.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2008 Workshops, 2008

Herbrand Sequent Extraction.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2006

Towards a clausal analysis of cut-elimination.

[BibT_eX]

[DOI]

J. Symb. Comput., 2006

Event-Related Outputs of Computations in P Systems.

[BibT_eX]

[DOI]

J. Autom. Lang. Comb., 2006

Proof Transformation by CERES.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

Proof Transformations and Structural Invariance.

[BibT_eX]

[DOI]

Proceedings of the Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006

2004

CERES in Many-Valued Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

Cut-Elimination: Experiments with CERES.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

2001

Comparing the Complexity of Cut-Elimination Methods.

[BibT_eX]

[DOI]

Proceedings of the Proof Theory in Computer Science, International Seminar, 2001

Resolution Decision Procedures.

[BibT_eX]

[DOI]

Ullrich Hustadt

Tanel Tammet

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Normal Form Transformations.

[BibT_eX]

[DOI]

Uwe Egly

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Cut-elimination and Redundancy-elimination by Resolution.

[BibT_eX]

[DOI]

J. Symb. Comput., 2000

1999

Cut Normal Forms and Proof Complexity.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1999

System Description: CutRes 0.1: Cut Elimination by Resolution.

[BibT_eX]

[DOI]

Georg Moser

Proceedings of the Automated Deduction, 1999

1998

Decision Procedures and Model Building in Equational Clause Logic.

[BibT_eX]

[DOI]

Log. J. IGPL, 1998

Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

1997

The Resolution Calculus.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Richard Zach

Theor. Comput. Sci., 1996

Hyperresolution and Automated Model Building.

[BibT_eX]

[DOI]

J. Log. Comput., 1996

Fast Cut-Elimination by Projection.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Richard Zach

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

On Skolemization and Proof Complexity.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1994

A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation

[BibT_eX]

[DOI]

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

1993

Deciding Clause Classes by Semantic Clash Resolution.

[BibT_eX]

Fundam. Informaticae, 1993

Resolution Methods for the Decision Problem

[BibT_eX]

[DOI]

Tanel Tammet

N. K. Zamov

Lecture Notes in Computer Science 679, Springer, ISBN: 3-540-56732-1, 1993

1992

Complexity of Resolution Proofs and Function Introduction.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1992

Model Building by Resolution.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 6th Workshop, 1992

1990

A Strong Problem Reduction Method Based on Function Introduction.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1990

1989

On Different Concepts of Resolution.

[BibT_eX]

[DOI]

Math. Log. Q., 1989

Deciding Horn Classes by Hyperresolution.

[BibT_eX]

[DOI]

Proceedings of the CSL '89, 1989

1987

Strong splitting rules in automated theorem proving.

[BibT_eX]

[DOI]

Proceedings of the EUROCAL '87, 1987

1985

On the Efficiency of Subsumption Algorithms

[BibT_eX]

[DOI]

Georg Gottlob

J. ACM, April, 1985

Eine Methode zur automatischen Problemreduktion.

[BibT_eX]

[DOI]

Proceedings of the Österreichische Artificial Intelligence-Tagung, 1985

Fast Subsumption Algorithms.

[BibT_eX]

[DOI]

Georg Gottlob

Proceedings of the EUROCAL '85, 1985

1982

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

[BibT_eX]

[DOI]

Computing, 1982

1980

Complexity of index sets and translating functions.

[BibT_eX]