| Publication | Date of Publication | Type |
|---|
| A strict constrained superposition calculus for graphs | 2023-11-24 | Paper |
| A proof procedure for separation logic with inductive definitions and data | 2023-10-24 | Paper |
| An undecidability result for separation logic with theory reasoning | 2023-06-05 | Paper |
| Unifying decidable entailments in separation logic with inductive definitions | 2021-12-01 | Paper |
| Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules | 2021-10-19 | Paper |
| The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates | 2020-09-11 | Paper |
| Prenex separation logic with one selector field | 2020-05-14 | Paper |
| Ilinva: using abduction to generate loop invariants | 2020-05-13 | Paper |
| Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL | 2020-04-07 | Paper |
| Combining induction and saturation-based theorem proving | 2020-03-03 | Paper |
| The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains | 2020-01-28 | Paper |
| A method for building models automatically. Experiments with an extension of OTTER | 2020-01-21 | Paper |
| Building proofs or counterexamples by analogy in a resolution framework | 2019-10-08 | Paper |
| Partial matching for analogy discovery in proofs and counter-examples | 2019-10-01 | Paper |
| Simplifying and generalizing formulae in tableaux. Pruning the search space and building models | 2019-01-15 | Paper |
| A tableaux calculus for reducing proof size | 2018-10-18 | Paper |
| A generic framework for implicate generation modulo theories | 2018-10-18 | Paper |
| Superposition with datatypes and codatatypes | 2018-10-18 | Paper |
| OUP accepted manuscript | 2018-02-13 | Paper |
| Prime Implicate Generation in Equational Logic | 2018-01-12 | Paper |
| The binomial pricing model in finance: a formalization in Isabelle | 2017-09-22 | Paper |
| A superposition calculus for abductive reasoning | 2017-08-17 | Paper |
| A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules | 2017-05-17 | Paper |
| Proof generalization in \(\mathrm {LK}\) by second order unifier minimization | 2016-10-27 | Paper |
| Analogy in Automated Deduction: A Survey | 2016-07-18 | Paper |
| Reasoning on Schemas of Formulas: An Automata-Based Approach | 2016-04-08 | Paper |
| Quantifier-Free Equational Logic and Prime Implicate Generation | 2015-12-02 | Paper |
| Instantiation Schemes for Nested Theories | 2015-09-17 | Paper |
| A complete superposition calculus for primal grammars | 2015-07-02 | Paper |
| Tractable and intractable classes of propositional schemata | 2015-02-11 | Paper |
| A Rewriting Strategy to Generate Prime Implicates in Equational Logic | 2014-09-26 | Paper |
| Schemata of Formulæ in the Theory of Arrays | 2013-10-04 | Paper |
| Combining Superposition and Induction: A Practical Realization | 2013-09-20 | Paper |
| A Resolution Calculus for First-order Schemata | 2013-08-26 | Paper |
| Completeness and Decidability Results for First-Order Clauses with Indices | 2013-06-14 | Paper |
| A Resolution-based Model Building Algorithm for a Fragment of OCC1N = | 2013-04-19 | Paper |
| Modular instantiation schemes | 2013-04-04 | Paper |
| Reasoning on Schemata of Formulæ | 2012-09-07 | Paper |
| A Calculus for Generating Ground Explanations | 2012-09-05 | Paper |
| An instantiation scheme for satisfiability modulo theories | 2012-07-31 | Paper |
| Schemata of SMT-Problems | 2011-07-01 | Paper |
| Decidability and Undecidability Results for Propositional Schemata | 2011-05-04 | Paper |
| Simplified handling of iterated term schemata | 2011-01-12 | Paper |
| A Decidable Class of Nested Iterated Schemata | 2010-09-14 | Paper |
| RegSTAB: A SAT Solver for Propositional Schemata | 2010-09-14 | Paper |
| Perfect Discrimination Graphs: Indexing Terms with Integer Exponents | 2010-09-14 | Paper |
| I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness | 2010-08-24 | Paper |
| Instantiation of SMT Problems Modulo Integers | 2010-08-24 | Paper |
| Complexity of the Satisfiability Problem for a Class of Propositional Schemata | 2010-05-26 | Paper |
| Automated Reasoning with Analytic Tableaux and Related Methods | 2010-03-09 | Paper |
| Bottom-up Construction of Semantic Tableaux | 2010-02-19 | Paper |
| Constructing infinite models represented by tree automata | 2009-12-11 | Paper |
| A Schemata Calculus for Propositional Logic | 2009-12-01 | Paper |
| A term-graph clausal logic: completeness and incompleteness results ★ | 2009-11-11 | Paper |
| Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps | 2009-03-10 | Paper |
| Automated Model Building: From Finite to Infinite Models | 2009-01-27 | Paper |
| Narrowing Data-Structures with Pointers | 2008-11-27 | Paper |
| Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview | 2008-11-07 | Paper |
| A Needed Rewriting Strategy for Data-Structures with Pointers | 2008-08-28 | Paper |
| Extended resolution simulates binary decision diagrams | 2008-03-28 | Paper |
| A Bottom-Up Approach to Clausal Tableaux | 2008-01-04 | Paper |
| Non Strict Confluent Rewrite Systems for Data-Structures with Pointers | 2008-01-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5294172 | 2007-07-24 | Paper |
| Some techniques for proving termination of the hyperresolution calculus | 2007-01-30 | Paper |
| Representing and building models for decidable subclasses of equational clausal logic | 2007-01-29 | Paper |
| Logics in Artificial Intelligence | 2006-10-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3372480 | 2006-02-21 | Paper |
| A Resolution Calculus for Shortening Proofs | 2005-10-18 | Paper |
| Automated model building | 2005-08-11 | Paper |
| The first order theory of primal grammars is decidable | 2004-10-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4430633 | 2003-10-12 | Paper |
| Model building with ordered resolution: Extracting models from saturated clause sets | 2003-08-25 | Paper |
| A calculus combining resolution and enumeration for building finite models | 2003-08-25 | Paper |
| Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae | 2003-08-24 | Paper |
| Extracting models from clause sets saturated under semantic refinements of the resolution rule. | 2003-08-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4530458 | 2002-11-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539642 | 2002-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4531862 | 2002-05-23 | Paper |
| On the decidability of the PVD class with equality | 2002-03-12 | Paper |
| Combining enumeration and deductive techniques in order to increase the class of constructible infinite models | 2001-03-19 | Paper |
| Pruning the search space and extracting more models in tableaux | 2000-12-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4250054 | 1999-06-17 | Paper |
| A new method for automated finite model building exploiting failures and symmetries | 1999-01-11 | Paper |
| Semantic generalizations for proving and disproving conjectures by analogy | 1998-06-02 | Paper |
| A new technique for verifying and correcting logic programs | 1997-11-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4349580 | 1997-08-24 | Paper |
| Increasing model building capabilities by constraint solving on terms with integer exponents | 1997-07-23 | Paper |
