| Publication | Date of Publication | Type |
|---|
| A fixed-point theorem for Horn formula equations | 2024-12-03 | Paper |
| Quantifier-free induction for lists | 2024-10-10 | Paper |
| Quantifier-free induction for lists | 2023-05-15 | Paper |
| Unprovability results for clause set cycles | 2022-10-14 | Paper |
| Induction and Skolemization in saturation theorem proving | 2022-10-14 | Paper |
| On the Herbrand content of LK | 2021-12-07 | Paper |
| Decidability of affine solution problems | 2021-10-21 | Paper |
| Induction and Skolemization in saturation theorem proving | 2021-05-17 | Paper |
| Clause set cycles and induction | 2020-12-15 | Paper |
| Cover complexity of finite languages | 2020-06-30 | Paper |
| Herbrand's theorem as higher order recursion | 2020-04-14 | Paper |
| Herbrand Confluence for First-Order Proofs with Π2-Cuts | 2020-04-02 | Paper |
| On the cover complexity of finite languages | 2019-11-07 | Paper |
| Expansion trees with cut | 2019-10-09 | Paper |
| Clause Set Cycles and Induction | 2019-10-09 | Paper |
| On the generation of quantified lemmas | 2019-05-31 | Paper |
| Complexity of decision problems on totally rigid acyclic tree grammars | 2018-11-22 | Paper |
| Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars | 2018-03-22 | Paper |
| On the compressibility of finite languages and formal proofs | 2018-03-21 | Paper |
| Some observations on the logical foundations of inductive theorem proving | 2017-12-11 | Paper |
| Functional Conceptual Substratum as a New Cognitive Mechanism for Mathematical Creation | 2017-10-11 | Paper |
| Tree grammars for the elimination of non-prenex cuts | 2017-08-31 | Paper |
| Herbrand disjunctions, cut elimination and context-free tree grammars | 2017-07-12 | Paper |
| Boolean unification with predicates | 2017-05-17 | Paper |
| System description: GAPT 2.0 | 2016-09-05 | Paper |
| A multi-focused proof system isomorphic to expansion proofs | 2016-07-07 | Paper |
| Book review of: D. W. Loveland et al., Three views of logic. Mathematics, philosophy, and computer science | 2016-01-07 | Paper |
| Compressibility of Finite Languages by Grammars | 2015-08-07 | Paper |
| Inductive theorem proving based on tree grammars | 2015-05-15 | Paper |
| Introducing quantified cuts in logic with equality | 2014-09-26 | Paper |
| Algorithmic introduction of quantified cuts | 2014-08-27 | Paper |
| Herbrand-confluence | 2014-01-08 | Paper |
| Understanding Resolution Proofs through Herbrand’s Theorem | 2013-10-04 | Paper |
| Expansion Trees with Cut | 2013-08-02 | Paper |
| The computational content of arithmetical proofs | 2012-11-23 | Paper |
| Herbrand-confluence for cut elimination in classical first order logic | 2012-11-22 | Paper |
| A systematic approach to canonicity in the classical sequent calculus | 2012-11-22 | Paper |
| Project presentation: algorithmic structuring and compression of proofs (ASCOP) | 2012-09-07 | Paper |
| On the complexity of proof deskolemization | 2012-06-19 | Paper |
| Towards Algorithmic Cut-Introduction | 2012-06-15 | Paper |
| Applying tree languages in proof theory | 2012-06-08 | Paper |
| CERES in higher-order logic | 2011-09-22 | Paper |
| On the non-confluence of cut-elimination | 2011-03-18 | Paper |
| A sequent calculus with implicit term representation | 2010-09-03 | Paper |
| On the form of witness terms | 2010-07-06 | Paper |
| Describing proofs by short tautologies | 2009-06-10 | Paper |
| A Clausal Approach to Proof Analysis in Second-Order Logic | 2009-02-24 | Paper |
| Herbrand Sequent Extraction | 2009-01-27 | Paper |
| CERES: An analysis of Fürstenberg's proof of the infinity of primes | 2008-09-16 | Paper |
| Proof Transformations and Structural Invariance | 2007-11-15 | Paper |
| Proof Transformation by CERES | 2007-09-05 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| On the Completeness of Interpolation Algorithms | N/A | Paper |
