| Publication | Date of Publication | Type |
|---|
| KBO Constraint Solving Revisited | 2024-05-03 | Paper |
| Symbolic Model Construction for Saturated Constrained Horn Clauses | 2024-05-03 | Paper |
| An Isabelle/HOL Formalization of the SCL(FOL) Calculus | 2024-04-26 | Paper |
| SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning | 2024-04-26 | Paper |
| SCL(EQ): SCL for first-order logic with equality | 2023-08-04 | Paper |
| A posthumous contribution by Larry Wos: excerpts from an unpublished column | 2022-12-12 | Paper |
| Semantic relevance | 2022-12-07 | Paper |
| An efficient subsumption test pipeline for BS(LRA) clauses | 2022-12-07 | Paper |
| Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL | 2022-12-07 | Paper |
| SCL(EQ): SCL for first-order logic with equality | 2022-12-07 | Paper |
| A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic | 2022-03-24 | Paper |
| Generalized completeness for SOS resolution and its application to a new notion of relevance | 2021-12-01 | Paper |
| Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories | 2021-10-18 | Paper |
| On the expressivity and applicability of model representation formalisms | 2020-05-13 | Paper |
| A complete and terminating approach to linear integer solving | 2020-03-24 | Paper |
| SPASS-SATT. A CDCL(LA) solver | 2020-03-10 | Paper |
| SCL clause learning from simple models | 2020-03-10 | Paper |
| SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment | 2020-03-03 | Paper |
| Soft typing for ordered resolution | 2019-10-01 | Paper |
| SPASS & FLOTTER version 0.42 | 2019-01-15 | Paper |
| Unification in pseudo-linear sort theories is decidable | 2019-01-15 | Paper |
| A verified SAT solver framework with learn, forget, restart, and incrementality | 2018-08-21 | Paper |
| Deciding First-Order Satisfiability when Universal and Existential Variables are Separated | 2018-04-23 | Paper |
| New techniques for linear arithmetic: cubes and equalities | 2018-01-08 | Paper |
| On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic | 2017-09-22 | Paper |
| Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints | 2017-09-22 | Paper |
| BDI: a new decidable clause class | 2017-05-17 | Paper |
| First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation | 2017-02-27 | Paper |
| NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment | 2017-02-27 | Paper |
| A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality | 2016-09-05 | Paper |
| Fast Cube Tests for LIA Constraint Solving | 2016-09-05 | Paper |
| Linear Integer Arithmetic Revisited | 2015-12-02 | Paper |
| Automated Reasoning Building Blocks | 2015-11-04 | Paper |
| Superposition for fixed domains | 2015-09-17 | Paper |
| Computing Tiny Clause Normal Forms | 2013-06-14 | Paper |
| Superposition as a decision procedure for timed automata | 2013-04-25 | Paper |
| Superposition decides the first-order logic fragment over ground theories | 2013-04-25 | Paper |
| From Search to Computation: Redundancy Criteria and Simplification at Work | 2013-04-19 | Paper |
| Harald Ganzinger’s Legacy: Contributions to Logics and Programming | 2013-04-19 | Paper |
| Superposition for Bounded Domains | 2013-04-16 | Paper |
| More SPASS with Isabelle | 2012-09-20 | Paper |
| A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance | 2012-09-05 | Paper |
| Combination of Disjoint Theories: Beyond Decidability | 2012-09-05 | Paper |
| Labelled Superposition for PLTL | 2012-06-15 | Paper |
| Automatic Generation of Invariants for Circular Derivations in SUP(LA) | 2012-06-15 | Paper |
| Superposition Modulo Non-linear Arithmetic | 2011-10-07 | Paper |
| First-Order Atom Definitions Extended | 2011-05-06 | Paper |
| Superposition-Based Analysis of First-Order Probabilistic Timed Automata | 2010-10-12 | Paper |
| On the Saturation of YAGO | 2010-09-14 | Paper |
| Subterm contextual rewriting | 2010-06-17 | Paper |
| Superposition modulo linear arithmetic SUP(LA) | 2010-01-07 | Paper |
| Labelled splitting | 2009-11-16 | Paper |
| Deciding the Inductive Validity of ∀ ∃ * Queries | 2009-11-12 | Paper |
| Decidability Results for Saturation-Based Model Building | 2009-07-28 | Paper |
| System Description: Spass Version 3.0 | 2009-03-06 | Paper |
| Labelled Clauses | 2009-03-06 | Paper |
| Labelled Splitting | 2008-11-27 | Paper |
| Superposition for Fixed Domains | 2008-11-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4809064 | 2004-08-12 | Paper |
| Computing small clause normal forms | 2002-08-27 | Paper |
| Combining superposition, sorts and splitting | 2001-10-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4524790 | 2001-01-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263167 | 2000-02-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4249904 | 1999-11-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4261067 | 1999-09-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3838762 | 1998-08-13 | Paper |
| Unification in sort theories and its applications | 1998-05-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4860657 | 1998-01-12 | Paper |
| A note on assumptions about Skolem functions | 1995-12-20 | Paper |
