| Publication | Date of Publication | Type |
|---|
| QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment | 2024-04-26 | Paper |
| Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover | 2023-06-14 | Paper |
| Completion procedures as semidecision procedures | 2023-03-09 | Paper |
| An application of automated equational reasoning to many-valued logic | 2023-03-09 | Paper |
| Larry Wos: visions of automated reasoning | 2022-12-12 | Paper |
| Set of support, demodulation, paramodulation: a historical perspective | 2022-12-12 | Paper |
| On fairness of completion-based theorem proving strategies | 2022-12-09 | Paper |
| SGGS decision procedures | 2022-11-09 | Paper |
| Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs | 2022-03-25 | Paper |
| Theory combination: beyond equality sharing | 2020-06-04 | Paper |
| Conflict-driven satisfiability for theory combination: transition system and completeness | 2020-03-03 | Paper |
| The Clause-Diffusion theorem prover Peers-mcd (system description) | 2019-10-01 | Paper |
| Semantically-guided goal-sensitive reasoning: inference system and completeness | 2018-04-03 | Paper |
| Satisfiability modulo theories and assignments | 2017-09-22 | Paper |
| Abstract canonical inference | 2017-07-12 | Paper |
| New results on rewrite-based satisfiability procedures | 2017-07-12 | Paper |
| Interpolation systems for ground proofs in automated deduction: a survey | 2016-05-26 | Paper |
| Semantically-guided goal-sensitive reasoning: model representation | 2016-05-26 | Paper |
| On First-Order Model-Based Reasoning | 2015-09-14 | Paper |
| On interpolation in automated theorem proving | 2015-07-02 | Paper |
| Rewrite-based satisfiability procedures for recursive data structures | 2013-12-06 | Paper |
| Rewrite-based decision procedures | 2013-12-06 | Paper |
| Canonical Ground Horn Theories | 2013-04-19 | Paper |
| On deciding satisfiability by theorem proving with speculative inferences | 2012-07-31 | Paper |
| On Interpolation in Decision Procedures | 2011-07-01 | Paper |
| Theory decision by decomposition | 2009-12-03 | Paper |
| On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving | 2009-07-28 | Paper |
| Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures | 2009-03-12 | Paper |
| ${\mathcal{T}}$ -Decision by Decomposition | 2009-03-06 | Paper |
| Canonical Inference for Implicational Systems | 2008-11-27 | Paper |
| On Variable-inactivity and Polynomial Formula-Satisfiability Procedures | 2008-03-12 | Paper |
| Towards a unified model of search in theorem-proving: subgoal-reduction strategies | 2007-10-19 | Paper |
| Frontiers of Combining Systems | 2006-10-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539630 | 2002-07-10 | Paper |
| A taxonomy of parallel strategies for deduction | 2002-06-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4941840 | 2002-04-30 | Paper |
| A model and a first analysis of distributed-search contraction-based strategies | 2000-06-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4246963 | 1999-06-16 | Paper |
| On the modelling of search in theorem proving -- towards a theory of strategy analysis | 1999-03-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4227007 | 1999-02-23 | Paper |
| PSATO: A distributed propositional prover and its application to quasigroup problems | 1997-06-16 | Paper |
| Towards a foundation of completion procedures as semidecision procedures | 1997-02-28 | Paper |
| On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method | 1997-02-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4847004 | 1996-05-28 | Paper |
| Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover | 1996-04-11 | Paper |
| On subsumption in distributed derivations | 1994-11-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4281516 | 1994-03-10 | Paper |
| On rewrite programs: Semantics and relationship with prolog | 1992-11-10 | Paper |
