| Publication | Date of Publication | Type |
|---|
| Schematic refutations of formula schemata | 2021-11-23 | Paper |
| An abstract form of the first epsilon theorem | 2020-12-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5219931 | 2020-03-09 | Paper |
| On the generation of quantified lemmas | 2019-05-31 | Paper |
| Extraction of expansion trees | 2019-03-20 | Paper |
| A Note on the Complexity of Classical and Intuitionistic Proofs | 2018-04-23 | Paper |
| A sequent-calculus based formulation of the extended first epsilon theorem | 2018-04-06 | Paper |
| OUP accepted manuscript | 2018-02-13 | Paper |
| The problem of \(\Pi_{2}\)-cut-introduction | 2017-11-16 | Paper |
| Ceres in intuitionistic logic | 2017-07-13 | Paper |
| Schematic Cut Elimination and the Ordered Pigeonhole Principle | 2016-09-05 | Paper |
| Cut-Elimination and Proof Schemata | 2015-12-03 | Paper |
| Cut-elimination: syntax and semantics | 2015-02-27 | Paper |
| Introducing Quantified Cuts in Logic with Equality | 2014-09-26 | Paper |
| Algorithmic introduction of quantified cuts | 2014-08-27 | Paper |
| Towards CERes in intuitionistic logic | 2012-11-22 | Paper |
| Towards Algorithmic Cut-Introduction | 2012-06-15 | Paper |
| CERES in higher-order logic | 2011-09-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3001091 | 2011-05-31 | Paper |
| Strong splitting rules in automated theorem proving | 2011-04-16 | Paper |
| Methods of cut-elimination | 2010-11-30 | Paper |
| System Description: The Proof Transformation System CERES | 2010-09-14 | Paper |
| A Clausal Approach to Proof Analysis in Second-Order Logic | 2009-02-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3597128 | 2009-02-09 | 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 |
| https://portal.mardi4nfdi.de/entity/Q3505121 | 2008-06-18 | Paper |
| Towards an algorithmic construction of cut-elimination procedures | 2008-04-10 | Paper |
| Proof Transformations and Structural Invariance | 2007-11-15 | Paper |
| Towards a clausal analysis of cut-elimination | 2007-10-23 | Paper |
| Proof Transformation by CERES | 2007-09-05 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5702660 | 2005-11-02 | Paper |
| Automated model building | 2005-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4436026 | 2003-11-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2751356 | 2002-08-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2751377 | 2001-10-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4524779 | 2001-07-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4942004 | 2001-03-19 | Paper |
| Cut-elimination and redundancy-elimination by resolution | 2001-03-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4503902 | 2000-09-14 | Paper |
| Cut normal forms and proof complexity | 2000-07-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4268482 | 1999-10-28 | Paper |
| Decision procedures and model building in equational clause logic | 1999-01-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4362908 | 1998-06-14 | Paper |
| Completeness of a first-order temporal logic with time-gaps | 1997-02-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4331764 | 1997-02-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4863690 | 1996-07-01 | Paper |
| Hyperresolution and automated model building | 1996-06-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4304753 | 1994-08-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3142019 | 1994-06-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4283235 | 1994-06-02 | Paper |
| Complexity of resolution proofs and function introduction | 1992-09-27 | Paper |
| On Different Concepts of Resolution | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4729408 | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4207882 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3716319 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3718690 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3727949 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3746919 | 1985-01-01 | Paper |
| On the efficiency of subsumption algorithms | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3693521 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3708002 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3330550 | 1983-01-01 | Paper |
| Decision-algorithms for the associativity of latin squares | 1983-01-01 | Paper |
| Fiducial intervals for the waiting time in batch and time-sharing systems | 1982-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3939791 | 1982-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3901506 | 1980-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3942946 | 1979-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4175546 | 1978-01-01 | Paper |
| Herbrand's Theorem in Refutation Schemata | 0001-01-03 | Paper |
