| Publication | Date of Publication | Type |
|---|
| Formalizing splitting in Isabelle/HOL | 2026-09-01 | Paper |
| A modular formalization of superposition in Isabelle/HOL | 2026-02-10 | Paper |
| Towards term-based verification of diagrammatic equivalence | 2026-01-01 | Paper |
| Verified Given Clause Procedures | 2024-04-26 | Paper |
Unifying splitting
Journal of Automated Reasoning | 2023-06-27 | Paper |
Superposition for higher-order logic
Journal of Automated Reasoning | 2023-06-14 | Paper |
A posthumous contribution by Larry Wos: excerpts from an unpublished column
Journal of Automated Reasoning | 2022-12-12 | Paper |
Making higher-order superposition work
Journal of Automated Reasoning | 2022-12-12 | Paper |
A comprehensive framework for saturation theorem proving
Journal of Automated Reasoning | 2022-12-12 | Paper |
Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL
(available as arXiv preprint) | 2022-12-07 | Paper |
A comprehensive framework for saturation theorem proving
Automated Reasoning | 2022-11-09 | Paper |
| Generalized completeness for SOS resolution and its application to a new notion of relevance | 2021-12-01 | Paper |
| A unifying splitting framework | 2021-12-01 | Paper |
| Superposition with first-class booleans and inprocessing clausification | 2021-12-01 | Paper |
| Superposition for full higher-order logic | 2021-12-01 | Paper |
Making higher-order superposition work
Automated Deduction – CADE 28 | 2021-12-01 | Paper |
Superposition with lambdas
Journal of Automated Reasoning | 2021-11-24 | Paper |
| Inductive learning from state transitions over continuous domains | 2021-02-08 | Paper |
Derivation reduction of metarules in meta-interpretive learning
Inductive Logic Programming | 2021-02-08 | Paper |
Logical reduction of metarules
Machine Learning | 2020-10-06 | Paper |
Superposition with lambdas
Lecture Notes in Computer Science | 2020-03-10 | Paper |
Superposition with lambdas
Lecture Notes in Computer Science | 2020-03-10 | Paper |
SLD-resolution reduction of second-order Horn fragments
(available as arXiv preprint) | 2020-02-18 | Paper |
| SLD-resolution reduction of second-order Horn fragments | 2020-02-18 | Paper |
Prime implicate generation in equational logic
Journal of Artificial Intelligence Research | 2018-01-12 | Paper |
Quantifier-free equational logic and prime implicate generation
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
A rewriting strategy to generate prime implicates in equational logic
Automated Reasoning | 2014-09-26 | Paper |
