| Publication | Date of Publication | Type |
|---|
| Computing ground congruence classes | 2026-01-21 | Paper |
| A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution | 2026-01-21 | Paper |
| A verified SAT solver framework including optimization and partial valuations | 2025-02-20 | Paper |
| Automatic bit- and memory-precise verification of eBPF code | 2025-02-19 | Paper |
| Exploring partial models with SCL | 2025-02-19 | Paper |
| First-order automatic literal model generation | 2025-01-31 | Paper |
| 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
Journal of Automated Reasoning | 2023-08-04 | Paper |
A posthumous contribution by Larry Wos: excerpts from an unpublished column
Journal of Automated Reasoning | 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
(available as arXiv preprint) | 2022-12-07 | Paper |
SCL(EQ): SCL for first-order logic with equality
(available as arXiv preprint) | 2022-12-07 | Paper |
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
(available as arXiv preprint) | 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
(available as arXiv preprint) | 2020-05-13 | Paper |
A complete and terminating approach to linear integer solving
Journal of Symbolic Computation | 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
Journal of Automated Reasoning | 2020-03-03 | Paper |
Soft typing for ordered resolution
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
SPASS \& FLOTTER version 0.42
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
Unification in pseudo-linear sort theories is decidable
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
A verified SAT solver framework with learn, forget, restart, and incrementality
Journal of Automated Reasoning | 2018-08-21 | Paper |
Deciding first-order satisfiability when universal and existential variables are separated
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
New techniques for linear arithmetic: cubes and equalities
Formal Methods in System Design | 2018-01-08 | Paper |
On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
(available as arXiv preprint) | 2017-09-22 | Paper |
Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints
(available as arXiv preprint) | 2017-09-22 | Paper |
BDI: a new decidable clause class
Journal Of Logic And Computation | 2017-05-17 | Paper |
First-order logic theorem proving and model building via approximation and instantiation
Frontiers of Combining Systems | 2017-02-27 | Paper |
NRCL -- a model building approach to the Bernays-Schönfinkel fragment
Frontiers of Combining Systems | 2017-02-27 | Paper |
NRCL -- a model building approach to the Bernays-Schönfinkel fragment
Frontiers of Combining Systems | 2017-02-27 | Paper |
A verified SAT solver framework with learn, forget, restart, and incrementality
Automated Reasoning | 2016-09-05 | Paper |
Fast cube tests for LIA constraint solving
Automated Reasoning | 2016-09-05 | Paper |
Linear integer arithmetic revisited
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Automated reasoning building blocks
Lecture Notes in Computer Science | 2015-11-04 | Paper |
Superposition for fixed domains
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Computing Tiny Clause Normal Forms
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
Superposition as a decision procedure for timed automata
Mathematics in Computer Science | 2013-04-25 | Paper |
Superposition decides the first-order logic fragment over ground theories
Mathematics in Computer Science | 2013-04-25 | Paper |
From search to computation: redundancy criteria and simplification at work
Programming Logics | 2013-04-19 | Paper |
Harald Ganzinger's legacy: contributions to logics and programming
Programming Logics | 2013-04-19 | Paper |
Superposition for bounded domains
Automated Reasoning and Mathematics | 2013-04-16 | Paper |
More SPASS with Isabelle
Interactive Theorem Proving | 2012-09-20 | Paper |
A PLTL-prover based on labelled superposition with partial model guidance
Automated Reasoning | 2012-09-05 | Paper |
Combination of disjoint theories: beyond decidability
Automated Reasoning | 2012-09-05 | Paper |
Labelled superposition for PLTL
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Automatic Generation of Invariants for Circular Derivations in SUP(LA)
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Superposition modulo non-linear arithmetic
Frontiers of Combining Systems | 2011-10-07 | Paper |
First-order atom definitions extended
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-05-06 | Paper |
Superposition-based analysis of first-order probabilistic timed automata
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
On the saturation of YAGO
Automated Reasoning | 2010-09-14 | Paper |
Subterm contextual rewriting
AI Communications | 2010-06-17 | Paper |
Superposition modulo linear arithmetic SUP(LA)
Frontiers of Combining Systems | 2010-01-07 | Paper |
Labelled splitting
Annals of Mathematics and Artificial Intelligence | 2009-11-16 | Paper |
Deciding the Inductive Validity of ∀ ∃ * Queries
Computer Science Logic | 2009-11-12 | Paper |
Decidability Results for Saturation-Based Model Building
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
System Description: Spass Version 3.0
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Labelled Clauses
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Labelled Splitting
Automated Reasoning | 2008-11-27 | Paper |
Superposition for Fixed Domains
Computer Science Logic | 2008-11-20 | Paper |
| scientific article; zbMATH DE number 2090305 (Why is no real title available?) | 2004-08-12 | Paper |
| Computing small clause normal forms | 2002-08-27 | Paper |
| Combining superposition, sorts and splitting | 2001-10-21 | Paper |
| scientific article; zbMATH DE number 1552530 (Why is no real title available?) | 2001-01-15 | Paper |
| scientific article; zbMATH DE number 1341618 (Why is no real title available?) | 2000-02-17 | Paper |
| scientific article; zbMATH DE number 1303351 (Why is no real title available?) | 1999-11-07 | Paper |
| scientific article; zbMATH DE number 1330426 (Why is no real title available?) | 1999-09-02 | Paper |
| scientific article; zbMATH DE number 1189060 (Why is no real title available?) | 1998-08-13 | Paper |
Unification in sort theories and its applications
Annals of Mathematics and Artificial Intelligence | 1998-05-17 | Paper |
| scientific article; zbMATH DE number 834570 (Why is no real title available?) | 1998-01-12 | Paper |
A note on assumptions about Skolem functions
Journal of Automated Reasoning | 1995-12-20 | Paper |
