| Publication | Date of Publication | Type |
|---|
| Closure properties of general grammars -- formally verified | 2024-11-26 | Paper |
| Seventeen provers under the hammer | 2024-07-15 | Paper |
| Recurrence-Driven Summations in Automated Deduction | 2024-05-03 | Paper |
| Verified Given Clause Procedures | 2024-04-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6123991 | 2024-04-08 | Paper |
| Extending a high-performance prover to higher-order logic | 2024-04-05 | Paper |
| SAT-Inspired Higher-Order Eliminations | 2023-08-26 | Paper |
| Unifying splitting | 2023-06-27 | Paper |
| Superposition for higher-order logic | 2023-06-14 | Paper |
| SAT-Inspired Eliminations for Superposition | 2023-02-07 | Paper |
| A comprehensive framework for saturation theorem proving | 2022-12-12 | Paper |
| Making higher-order superposition work | 2022-12-12 | Paper |
| A comprehensive framework for saturation theorem proving | 2022-11-09 | Paper |
| A unifying splitting framework | 2021-12-01 | Paper |
| Superposition for full higher-order logic | 2021-12-01 | Paper |
| Making higher-order superposition work | 2021-12-01 | Paper |
| Superposition with lambdas | 2021-11-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4989394 | 2021-05-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5144617 | 2021-01-19 | Paper |
| Formalizing Bachmair and Ganzinger's ordered resolution prover | 2020-11-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111307 | 2020-05-26 | Paper |
| Superposition with lambdas | 2020-03-10 | Paper |
| Scalable fine-grained proofs for formula processing | 2020-03-03 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
| A formal proof of the expressiveness of deep learning | 2019-08-21 | Paper |
| Formalizing Bachmair and Ganzinger's ordered resolution prover | 2018-10-18 | Paper |
| Superposition for \(\lambda\)-free higher-order logic | 2018-10-18 | Paper |
| Superposition with datatypes and codatatypes | 2018-10-18 | Paper |
| A verified SAT solver framework with learn, forget, restart, and incrementality | 2018-08-21 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | Paper |
| A formal proof of the expressiveness of deep learning | 2018-01-04 | Paper |
| A transfinite Knuth-Bendix order for lambda-free higher-order terms | 2017-09-22 | Paper |
| Scalable fine-grained proofs for formula processing | 2017-09-22 | Paper |
| Soundness and completeness proofs by coinductive methods | 2017-07-10 | Paper |
| A decision procedure for (co)datatypes in SMT solvers | 2017-06-29 | Paper |
| Friends with Benefits | 2017-05-19 | Paper |
| A Lambda-Free Higher-Order Recursive Path Order | 2017-05-19 | Paper |
| Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving | 2017-05-16 | Paper |
| Foundational extensible corecursion: a proof assistant perspective | 2017-05-10 | Paper |
| Encoding Monomorphic and Polymorphic Types | 2017-04-11 | Paper |
| A learning-based fact selector for Isabelle/HOL | 2016-10-27 | Paper |
| Model Finding for Recursive Functions in SMT | 2016-09-05 | Paper |
| A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality | 2016-09-05 | Paper |
| Semi-intelligible Isar proofs from machine-generated proofs | 2016-05-26 | Paper |
| Witnessing (Co)datatypes | 2016-04-26 | Paper |
| A Decision Procedure for (Co)datatypes in SMT Solvers | 2015-12-02 | Paper |
| Mining the Archive of Formal Proofs | 2015-11-20 | Paper |
| Extending Sledgehammer with SMT solvers | 2015-06-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4982446 | 2015-04-09 | Paper |
| Unified Classical Logic Completeness | 2014-09-26 | Paper |
| Truly Modular (Co)datatypes for Isabelle/HOL | 2014-09-08 | Paper |
| Cardinals in Isabelle/HOL | 2014-09-08 | Paper |
| Mechanizing the Metatheory of Sledgehammer | 2013-09-20 | Paper |
| MaSh: Machine Learning for Sledgehammer | 2013-08-07 | Paper |
| Encoding Monomorphic and Polymorphic Types | 2013-08-05 | Paper |
| TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism | 2013-06-14 | Paper |
| LEO-II and Satallax on the Sledgehammer test bench | 2013-05-02 | Paper |
| More SPASS with Isabelle | 2012-09-20 | Paper |
| Monotonicity inference for higher-order formulas | 2012-07-31 | Paper |
| Automatic Proof and Disproof in Isabelle/HOL | 2011-10-07 | Paper |
| Extending Sledgehammer with SMT Solvers | 2011-07-29 | Paper |
| Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models | 2010-10-12 | Paper |
| Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder | 2010-09-14 | Paper |
| Monotonicity Inference for Higher-Order Formulas | 2010-09-14 | Paper |
| Proof pearl: Mechanizing the textbook proof of Huffman's algorithm | 2009-09-01 | Paper |
