| Publication | Date of Publication | Type |
|---|
| Merging relational database technology with constraint technology | 2024-07-11 | Paper |
| Simultaneous rigid E-unification is undecidable | 2024-06-21 | Paper |
| Program Synthesis in Saturation | 2024-04-26 | Paper |
| ALASCA: reasoning in quantified linear arithmetic | 2023-12-13 | Paper |
| Getting saturated with induction | 2023-08-10 | Paper |
| Testing a Saturation-Based Theorem Prover: Experiences and Challenges | 2022-07-01 | Paper |
| Inductive benchmarks for automated reasoning | 2022-04-22 | Paper |
| Integer induction in saturation | 2021-12-01 | Paper |
| Making theory reasoning simpler | 2021-10-18 | Paper |
| Induction with generalization in superposition reasoning | 2021-01-20 | Paper |
| Induction in saturation-based proof search | 2020-03-10 | Paper |
| What you always wanted to know about rigid E-unification | 2019-10-08 | Paper |
| Unification with abstraction and theory instantiation in saturation-based reasoning | 2019-09-16 | Paper |
| Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification | 2019-01-15 | Paper |
| Proof-search in intuitionistic logic based on constraint satisfaction | 2019-01-10 | Paper |
| First-Order Interpolation and Interpolating Proof Systems | 2019-01-10 | Paper |
| A FOOLish encoding of the next state relations of imperative programs | 2018-10-18 | Paper |
| Monadic simultaneous rigid E-unification and related problems | 2018-07-04 | Paper |
| Coming to terms with quantified reasoning | 2017-10-20 | Paper |
| Knuth--bendix constraint solving is NP-complete | 2017-07-12 | Paper |
| Selecting the Selection | 2016-09-05 | Paper |
| Finding Finite Models in Multi-sorted First-Order Logic | 2016-09-05 | Paper |
| Extensional Crisis and Proving Identity | 2015-12-17 | Paper |
| GoRRiLA and Hard Reality | 2015-12-07 | Paper |
| Implementing Conflict Resolution | 2015-12-07 | Paper |
| Playing with AVATAR | 2015-12-02 | Paper |
| Cooperating Proof Attempts | 2015-12-02 | Paper |
| A First Class Boolean Sort in First-Order Theorem Proving and TPTP | 2015-11-20 | Paper |
| Playing in the grey area of proofs | 2015-09-11 | Paper |
| AVATAR: The Architecture for First-Order Theorem Provers | 2014-09-29 | Paper |
| The 481 Ways to Split a Clause and Deal with Propositional Variables | 2013-06-14 | Paper |
| Planning with Effectively Propositional Logic | 2013-04-19 | Paper |
| Harald Ganzinger’s Legacy: Contributions to Logics and Programming | 2013-04-19 | Paper |
| EPR-Based Bounded Model Checking at Word Level | 2012-09-05 | Paper |
| Translating regular expression matching into transducers | 2012-05-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3108190 | 2012-01-01 | Paper |
| Sine Qua Non for Large Theory Reasoning | 2011-07-29 | Paper |
| On Transfinite Knuth-Bendix Orders | 2011-07-29 | Paper |
| Solving Systems of Linear Inequalities by Bound Propagation | 2011-07-29 | Paper |
| Interpolation and Symbol Elimination in Vampire | 2010-09-14 | Paper |
| Evaluation of Automated Theorem Proving on the Mizar Mathematical Library | 2010-09-14 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Invariant and Type Inference for Matrices | 2010-01-14 | Paper |
| Perspectives of System Informatics | 2010-01-05 | Paper |
| How to optimize proof-search in modal logics | 2009-10-21 | Paper |
| A decision procedure for term algebras with queues | 2009-10-21 | Paper |
| Conflict Resolution | 2009-10-09 | Paper |
| Inter-program Properties | 2009-08-18 | Paper |
| Interpolation and Symbol Elimination | 2009-07-28 | Paper |
| Path Feasibility Analysis for String-Manipulating Programs | 2009-03-31 | Paper |
| Encodings of Bounded LTL Model Checking in Effectively Propositional Logic | 2009-03-06 | Paper |
| Integrating Linear Arithmetic into Superposition Calculus | 2009-03-05 | Paper |
| Proof Systems for Effectively Propositional Logic | 2008-11-27 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| Computer Science Logic | 2007-06-21 | Paper |
| Computer Science Logic | 2007-06-21 | Paper |
| Foundations of Information and Knowledge Systems | 2007-02-12 | Paper |
| Static Analysis | 2006-10-31 | Paper |
| Mathematical Foundations of Computer Science 2005 | 2006-10-20 | Paper |
| Mathematical Foundations of Computer Science 2005 | 2006-10-20 | Paper |
| Mechanizing Mathematical Reasoning | 2006-01-10 | Paper |
| Efficient instance retrieval with standard and relational path indexing | 2005-08-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3043806 | 2004-08-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4449214 | 2004-02-08 | Paper |
| Limited resource strategy in resolution theorem proving | 2003-08-25 | Paper |
| Stratified resolution | 2003-08-25 | Paper |
| Orienting rewrite rules with the Knuth-Bendix order. | 2003-08-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4415258 | 2003-07-28 | Paper |
| Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification | 2003-06-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4806209 | 2003-05-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4536327 | 2002-11-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3150300 | 2002-09-30 | Paper |
| Term-modal logics | 2002-09-16 | Paper |
| The inverse method | 2002-08-27 | Paper |
| Equality reasoning in sequent-based calculi | 2002-07-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539610 | 2002-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539595 | 2002-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539622 | 2002-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4535077 | 2002-06-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2778876 | 2002-03-21 | Paper |
| Term indexing | 2001-10-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723432 | 2001-07-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2721198 | 2001-07-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4790398 | 2001-01-01 | Paper |
| The ground-negative fragment of first-order logic is -complete | 2000-07-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4936130 | 2000-01-24 | Paper |
| Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem | 2000-01-12 | Paper |
| Monadic simultaneous rigid \(E\)-unification | 2000-01-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4264724 | 1999-10-10 | Paper |
| Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification | 1999-09-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4264062 | 1999-09-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4249897 | 1999-09-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4260706 | 1999-09-01 | Paper |
| What you always wanted to know about rigid \(E\)-unification | 1998-08-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3838767 | 1998-08-13 | Paper |
| A note on semantics of logic programs with equality based on complete sets of E-unifiers | 1997-11-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3129297 | 1997-04-27 | Paper |
| The undecidability of simultaneous rigid E-unification | 1997-02-27 | Paper |
| On computability by logic programs | 1996-10-20 | Paper |
| The anatomy of vampire. Implementing bottom-up procedures with code trees | 1995-12-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4282616 | 1994-08-21 | Paper |
