Stefan Hetzl

Sebastian Zivota

J. Log. Comput., 2020

Clause Set Cycles and Induction.

[BibT_eX]

[DOI]

Jannik Vierling

Log. Methods Comput. Sci., 2020

Herbrand's theorem as higher order recursion.

[BibT_eX]

[DOI]

Bahareh Afshari

Graham E. Leigh

Ann. Pure Appl. Log., 2020

2019

On the cover complexity of finite languages.

[BibT_eX]

[DOI]

Simon Wolfsteiner

Theor. Comput. Sci., 2019

Expansion trees with cut.

[BibT_eX]

[DOI]

Federico Aschieri

Math. Struct. Comput. Sci., 2019

On the Generation of Quantified Lemmas.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

2018

On the compressibility of finite languages and formal proofs.

[BibT_eX]

[DOI]

Inf. Comput., 2018

Complexity of Decision Problems on Totally Rigid Acyclic Tree Grammars.

[BibT_eX]

[DOI]

Gabriel Ebner

Proceedings of the Developments in Language Theory - 22nd International Conference, 2018

2017

Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars.

[BibT_eX]

[DOI]

Gabriel Ebner

ACM Trans. Comput. Log., 2017

Boolean unification with predicates.

[BibT_eX]

[DOI]

J. Log. Comput., 2017

Preface.

[BibT_eX]

[DOI]

J. Log. Comput., 2017

Some observations on the logical foundations of inductive theorem proving.

[BibT_eX]

[DOI]

Tin Lok Wong

Log. Methods Comput. Sci., 2017

Restricted notions of provability by induction.

[BibT_eX]

[DOI]

Tin Lok Wong

CoRR, 2017

2016

A multi-focused proof system isomorphic to expansion proofs.

[BibT_eX]

[DOI]

Kaustuv Chaudhuri

Dale Miller

J. Log. Comput., 2016

On the Herbrand content of LK.

[BibT_eX]

[DOI]

Bahareh Afshari

Graham E. Leigh

Proceedings of the Proceedings Sixth International Workshop on Classical Logic and Computation, 2016

System Description: GAPT 2.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Inductive theorem proving based on tree grammars.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2015

Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars.

[BibT_eX]

[DOI]

Bahareh Afshari

Graham Emil Leigh

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

Compressibility of Finite Languages by Grammars.

[BibT_eX]

[DOI]

Proceedings of the Descriptional Complexity of Formal Systems, 2015

Tree Grammars for the Elimination of Non-prenex Cuts.

[BibT_eX]

[DOI]

Sebastian Zivota

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

Algorithmic introduction of quantified cuts.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2014

The Cayley-Hamilton Theorem.

[BibT_eX]

[DOI]

Stephan Adelsberger

Florian Pollak

Arch. Formal Proofs, 2014

Introducing Quantified Cuts in Logic with Equality.

[BibT_eX]

[DOI]

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

2013

Expansion Trees with Cut.

[BibT_eX]

[DOI]

CoRR, 2013

Herbrand-Confluence.

[BibT_eX]

[DOI]

Lutz Straßburger

Log. Methods Comput. Sci., 2013

Understanding Resolution Proofs through Herbrand's Theorem.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

2012

The Computational Content of Arithmetical Proofs.

[BibT_eX]

[DOI]

Notre Dame J. Formal Log., 2012

On the complexity of proof deskolemization.

[BibT_eX]

[DOI]

Matthias Baaz

J. Symb. Log., 2012

Bondy's Theorem.

[BibT_eX]

[DOI]

Jeremy Avigad

Arch. Formal Proofs, 2012

Towards Algorithmic Cut-Introduction.

[BibT_eX]

[DOI]

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

Applying Tree Languages in Proof Theory.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2012

Herbrand-Confluence for Cut Elimination in Classical First Order Logic.

[BibT_eX]

[DOI]

Lutz Straßburger

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

A Systematic Approach to Canonicity in the Classical Sequent Calculus.

[BibT_eX]

[DOI]

Kaustuv Chaudhuri

Dale Miller

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

Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP).

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

On the non-confluence of cut-elimination.

[BibT_eX]

[DOI]

Matthias Baaz

J. Symb. Log., 2011

CERES in higher-order logic.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2011

2010

On the form of witness terms.

[BibT_eX]

[DOI]

Arch. Math. Log., 2010

A Sequent Calculus with Implicit Term Representation.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

Describing proofs by short tautologies.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2009

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

[BibT_eX]

[DOI]

Bruno Woltzenlogel Paleo

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

Transforming and Analyzing Proofs in the CERES-System.

[BibT_eX]

[DOI]

Bruno Woltzenlogel Paleo

Proceedings of the LPAR 2008 Workshops, 2008

Herbrand Sequent Extraction.

[BibT_eX]

[DOI]

Bruno Woltzenlogel Paleo

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

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

2005

A Graph-Theoretic Approach to Steganography.

[BibT_eX]

[DOI]