| Publication | Date of Publication | Type |
|---|
| Computing witnesses using the SCAN algorithm | 2026-01-21 | Paper |
| A fixed-point theorem for Horn formula equations | 2024-12-03 | Paper |
Quantifier-free induction for lists
Archive for Mathematical Logic | 2024-10-10 | Paper |
| Quantifier-free induction for lists | 2023-05-15 | Paper |
Unprovability results for clause set cycles
Theoretical Computer Science | 2022-10-14 | Paper |
Induction and Skolemization in saturation theorem proving
Annals of Pure and Applied Logic | 2022-10-14 | Paper |
| On the Herbrand content of LK | 2021-12-07 | Paper |
On the Herbrand content of LK
(available as arXiv preprint) | 2021-12-07 | Paper |
Decidability of affine solution problems
Journal Of Logic And Computation | 2021-10-21 | Paper |
Induction and Skolemization in saturation theorem proving
(available as arXiv preprint) | 2021-05-17 | Paper |
Clause set cycles and induction
(available as arXiv preprint) | 2020-12-15 | 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
Annals of Pure and Applied Logic | 2020-04-14 | Paper |
Herbrand Confluence for First-Order Proofs with Π2-Cuts
Concepts of Proof in Mathematics, Philosophy, and Computer Science | 2020-04-02 | Paper |
On the cover complexity of finite languages
Theoretical Computer Science | 2019-11-07 | Paper |
Expansion trees with cut
Mathematical Structures in Computer Science | 2019-10-09 | Paper |
Clause Set Cycles and Induction
(available as arXiv preprint) | 2019-10-09 | Paper |
On the generation of quantified lemmas
Journal of Automated Reasoning | 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
ACM Transactions on Computational Logic | 2018-03-22 | Paper |
On the compressibility of finite languages and formal proofs
Information and Computation | 2018-03-21 | Paper |
Some observations on the logical foundations of inductive theorem proving
(available as arXiv preprint) | 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
Journal Of Logic And Computation | 2017-05-17 | Paper |
System description: GAPT 2.0
Automated Reasoning | 2016-09-05 | Paper |
A multi-focused proof system isomorphic to expansion proofs
Journal Of Logic And Computation | 2016-07-07 | Paper |
Book review of: D. W. Loveland et al., Three views of logic. Mathematics, philosophy, and computer science
Mathematische Semesterberichte | 2016-01-07 | Paper |
Compressibility of Finite Languages by Grammars
Descriptional Complexity of Formal Systems | 2015-08-07 | Paper |
Inductive theorem proving based on tree grammars
Annals of Pure and Applied Logic | 2015-05-15 | Paper |
Introducing quantified cuts in logic with equality
Automated Reasoning | 2014-09-26 | Paper |
Algorithmic introduction of quantified cuts
Theoretical Computer Science | 2014-08-27 | Paper |
Herbrand-confluence
Logical Methods in Computer Science | 2014-01-08 | Paper |
Understanding Resolution Proofs through Herbrand’s Theorem
Lecture Notes in Computer Science | 2013-10-04 | Paper |
| Expansion Trees with Cut | 2013-08-02 | Paper |
The computational content of arithmetical proofs
Notre Dame Journal of Formal Logic | 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)
Lecture Notes in Computer Science | 2012-09-07 | Paper |
On the complexity of proof deskolemization
The Journal of Symbolic Logic | 2012-06-19 | Paper |
Towards Algorithmic Cut-Introduction
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Applying tree languages in proof theory
Language and Automata Theory and Applications | 2012-06-08 | Paper |
CERES in higher-order logic
Annals of Pure and Applied Logic | 2011-09-22 | Paper |
On the non-confluence of cut-elimination
Journal of Symbolic Logic | 2011-03-18 | Paper |
A sequent calculus with implicit term representation
Computer Science Logic | 2010-09-03 | Paper |
On the form of witness terms
Archive for Mathematical Logic | 2010-07-06 | Paper |
Describing proofs by short tautologies
Annals of Pure and Applied Logic | 2009-06-10 | Paper |
A Clausal Approach to Proof Analysis in Second-Order Logic
Logical Foundations of Computer Science | 2009-02-24 | Paper |
Herbrand Sequent Extraction
Lecture Notes in Computer Science | 2009-01-27 | Paper |
CERES: An analysis of Fürstenberg's proof of the infinity of primes
Theoretical Computer Science | 2008-09-16 | Paper |
Proof Transformations and Structural Invariance
Lecture Notes in Computer Science | 2007-11-15 | Paper |
Proof Transformation by CERES
Lecture Notes in Computer Science | 2007-09-05 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
On the Completeness of Interpolation Algorithms
(available as arXiv preprint) | N/A | Paper |
