| 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 |
| Finding mathematical proofs using computers | 2024-04-08 | Paper |
| Extending a high-performance prover to higher-order logic | 2024-04-05 | Paper |
SAT-Inspired Higher-Order Eliminations
Logical Methods in Computer Science | 2023-08-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 |
SAT-Inspired Eliminations for Superposition
ACM Transactions on Computational Logic | 2023-02-07 | Paper |
A comprehensive framework for saturation theorem proving
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
Automated Reasoning | 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
Automated Deduction – CADE 28 | 2021-12-01 | Paper |
Superposition with lambdas
Journal of Automated Reasoning | 2021-11-24 | Paper |
scientific article; zbMATH DE number 7350767 (Why is no real title available?)
(available as arXiv preprint) | 2021-05-25 | Paper |
| scientific article; zbMATH DE number 7350767 (Why is no real title available?) | 2021-05-25 | Paper |
| Foundational nonuniform (co)datatypes for higher-order logic | 2021-01-19 | Paper |
Formalizing Bachmair and Ganzinger's ordered resolution prover
Journal of Automated Reasoning | 2020-11-02 | Paper |
| scientific article; zbMATH DE number 7204430 (Why is no real title available?) | 2020-05-26 | 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 |
Scalable fine-grained proofs for formula processing
Journal of Automated Reasoning | 2020-03-03 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
A formal proof of the expressiveness of deep learning
Journal of Automated Reasoning | 2019-08-21 | Paper |
Formalizing Bachmair and Ganzinger's ordered resolution prover
Automated Reasoning | 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
Journal of Automated Reasoning | 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
Interactive Theorem Proving | 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
Automated Deduction – CADE 26 | 2017-09-22 | Paper |
Soundness and completeness proofs by coinductive methods
Journal of Automated Reasoning | 2017-07-10 | Paper |
A decision procedure for (co)datatypes in SMT solvers
Journal of Automated Reasoning | 2017-06-29 | Paper |
Friends with benefits. Implementing corecursion in foundational proof assistants
Programming Languages and Systems | 2017-05-19 | Paper |
A Lambda-Free Higher-Order Recursive Path Order
Lecture Notes in Computer Science | 2017-05-19 | Paper |
Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
Foundational extensible corecursion: a proof assistant perspective
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
Foundational extensible corecursion: a proof assistant perspective
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
Encoding monomorphic and polymorphic types
Logical Methods in Computer Science | 2017-04-11 | Paper |
A learning-based fact selector for Isabelle/HOL
Journal of Automated Reasoning | 2016-10-27 | Paper |
Model finding for recursive functions in SMT
Automated Reasoning | 2016-09-05 | Paper |
A verified SAT solver framework with learn, forget, restart, and incrementality
Automated Reasoning | 2016-09-05 | Paper |
Semi-intelligible Isar proofs from machine-generated proofs
Journal of Automated Reasoning | 2016-05-26 | Paper |
Witnessing (co)datatypes
Programming Languages and Systems | 2016-04-26 | Paper |
A decision procedure for (co)datatypes in SMT solvers
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Mining the Archive of Formal Proofs
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Extending Sledgehammer with SMT solvers
Journal of Automated Reasoning | 2015-06-23 | Paper |
| scientific article; zbMATH DE number 6423829 (Why is no real title available?) | 2015-04-09 | Paper |
Unified Classical Logic Completeness
Automated Reasoning | 2014-09-26 | Paper |
Truly modular (co)datatypes for Isabelle/HOL
Interactive Theorem Proving | 2014-09-08 | Paper |
Cardinals in Isabelle/HOL
Interactive Theorem Proving | 2014-09-08 | Paper |
Mechanizing the metatheory of Sledgehammer
Frontiers of Combining Systems | 2013-09-20 | Paper |
MaSh: machine learning for Sledgehammer
Interactive Theorem Proving | 2013-08-07 | Paper |
Encoding monomorphic and polymorphic types
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
LEO-II and Satallax on the Sledgehammer test bench
Journal of Applied Logic | 2013-05-02 | Paper |
More SPASS with Isabelle
Interactive Theorem Proving | 2012-09-20 | Paper |
Monotonicity inference for higher-order formulas
Journal of Automated Reasoning | 2012-07-31 | Paper |
Automatic proof and disproof in Isabelle/HOL
Frontiers of Combining Systems | 2011-10-07 | Paper |
Extending Sledgehammer with SMT solvers
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Generating counterexamples for structural inductions by exploiting nonstandard models
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Nitpick: a counterexample generator for higher-order logic based on a relational model finder
Interactive Theorem Proving | 2010-09-14 | Paper |
Monotonicity inference for higher-order formulas
Automated Reasoning | 2010-09-14 | Paper |
Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
Journal of Automated Reasoning | 2009-09-01 | Paper |
