| Publication | Date of Publication | Type |
|---|
| Number theory combination: natural density and SMT | 2026-02-26 | Paper |
| Shininess, strong politeness, and unicorns | 2026-02-26 | Paper |
Combining combination properties. I: Nelson-Oppen and politeness
Journal of Automated Reasoning | 2026-02-06 | Paper |
| Being polite is not enough (and other limits of theory combination) | 2026-01-21 | Paper |
| DNN verification, reachability, and the exponential function problem | 2025-06-26 | Paper |
| Combining combination properties: minimal models | 2025-02-19 | Paper |
| Formal Verification of Bit-Vector Invertibility Conditions in Coq | 2024-05-03 | Paper |
| Combining Finite Combination Properties: Finite Models and Busy Beavers | 2024-05-03 | Paper |
Combining stable infiniteness and (strong) politeness
Journal of Automated Reasoning | 2023-10-24 | Paper |
Reasoning about vectors: satisfiability modulo a theory of sequences
Journal of Automated Reasoning | 2023-10-24 | Paper |
| Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness | 2023-05-03 | Paper |
| Flexible proof production in an industrial-strength SMT solver | 2022-12-07 | Paper |
Reasoning about vectors using an SMT theory of sequences
(available as arXiv preprint) | 2022-12-07 | Paper |
| Effective semantics for the modal logics K and KT via non-deterministic matrices | 2022-12-07 | Paper |
| Politeness for the theory of algebraic datatypes | 2022-11-09 | Paper |
Polite combination of algebraic datatypes
Journal of Automated Reasoning | 2022-10-24 | Paper |
Smt-Switch: a solver-agnostic C++ API for SMT solving
(available as arXiv preprint) | 2022-03-22 | Paper |
Politeness and stable infiniteness: stronger together
(available as arXiv preprint) | 2021-12-01 | Paper |
Towards satisfiability modulo parametric bit-vectors
Journal of Automated Reasoning | 2021-11-24 | Paper |
Modal extension of ideal paraconsistent four-valued logic and its subsystem
Annals of Pure and Applied Logic | 2020-10-07 | Paper |
Completeness and cut-elimination for first-order ideal paraconsistent four-valued logic
Studia Logica | 2020-06-09 | Paper |
| Automating automated reasoning. The case of two generic automated reasoning tools | 2020-06-04 | Paper |
DRAT-based bit-vector proofs in CVC4
(available as arXiv preprint) | 2020-05-20 | Paper |
Towards bit-width-independent proofs in SMT solvers
(available as arXiv preprint) | 2020-03-10 | Paper |
Towards automated reasoning in Herbrand structures
Journal Of Logic And Computation | 2020-02-03 | Paper |
Pure sequent calculi. Analyticity and decision procedure
ACM Transactions on Computational Logic | 2019-11-22 | Paper |
Yet another paradefinite logic: The role of conflation1
Logic Journal of the IGPL | 2019-11-04 | Paper |
REXPANSIONS OF NONDETERMINISTIC MATRICES AND THEIR APPLICATIONS IN NONCLASSICAL LOGICS
The Review of Symbolic Logic | 2019-06-07 | Paper |
From the subformula property to cut-admissibility in propositional sequent calculi
Journal Of Logic And Computation | 2019-01-31 | Paper |
scientific article; zbMATH DE number 6863659 (Why is no real title available?)
(available as arXiv preprint) | 2018-04-23 | Paper |
| Cut-admissibility as a corollary of the subformula property | 2018-02-02 | Paper |
Sequent systems for negative modalities
Logica Universalis | 2017-11-29 | Paper |
Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi
Automated Reasoning | 2016-09-05 | Paper |
On the construction of analytic sequent calculi for sub-classical logics
Logic, Language, Information, and Computation | 2015-01-13 | Paper |
SAT-based decision procedure for analytic pure sequent calculi
Automated Reasoning | 2014-09-26 | Paper |
