| Publication | Date of Publication | Type |
|---|
| Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project | 2024-02-28 | Paper |
| A concrete final coalgebra theorem for ZF set theory | 2023-12-08 | Paper |
| A formalised theorem in the partition calculus | 2023-10-12 | Paper |
| Formalising Mathematics in Simple Type Theory | 2023-09-20 | Paper |
| Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover | 2023-08-31 | Paper |
| Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL | 2023-06-14 | Paper |
| Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis | 2023-06-02 | Paper |
| Bayesian ranking for strategy scheduling in automated theorem provers | 2022-12-07 | Paper |
| Algebraically Closed Fields in Isabelle/HOL | 2022-11-09 | Paper |
| Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types | 2022-08-03 | Paper |
| Formalizing Ordinal Partition Relations Using Isabelle/HOL | 2022-08-03 | Paper |
| Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL | 2022-08-03 | Paper |
| A modular first formalisation of combinatorial design theory | 2022-04-22 | Paper |
| ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT | 2022-03-01 | Paper |
| Formalising Ordinal Partition Relations Using Isabelle/HOL | 2020-11-26 | Paper |
| Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL | 2020-03-03 | Paper |
| A fixedpoint approach to implementing (Co)inductive definitions | 2020-01-21 | Paper |
| From LCF to Isabelle/HOL | 2019-12-18 | Paper |
| Using machine learning to improve cylindrical algebraic decomposition | 2019-11-27 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
| An Isabelle/HOL formalisation of Green's theorem | 2019-09-02 | Paper |
| Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL | 2019-02-15 | Paper |
| Computational logic: its origins and applications | 2018-12-04 | Paper |
| Defining functions on equivalence classes | 2017-07-12 | Paper |
| Mechanizing UNITY in Isabelle | 2017-06-13 | Paper |
| Proofs and Reconstructions | 2017-02-27 | Paper |
| An Isabelle/HOL Formalisation of Green’s Theorem | 2016-10-27 | Paper |
| A Formal Proof of Cauchy’s Residue Theorem | 2016-10-27 | Paper |
| Automated theorem proving for special functions | 2016-09-29 | Paper |
| A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle | 2016-05-26 | Paper |
| The higher-order prover \textsc{Leo}-II | 2016-05-26 | Paper |
| A Formalisation of Finite Automata Using Hereditarily Finite Sets | 2015-12-02 | Paper |
| Extending Sledgehammer with SMT solvers | 2015-06-23 | Paper |
| Machine learning for first-order theorem proving | 2015-06-23 | Paper |
| A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS | 2015-01-21 | Paper |
| Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition | 2014-08-07 | Paper |
| MetiTarski’s Menagerie of Cooperating Systems | 2013-09-20 | Paper |
| Case splitting in an automatic theorem prover for real-valued special functions | 2013-07-05 | Paper |
| LEO-II and Satallax on the Sledgehammer test bench | 2013-05-02 | Paper |
| Quantified multimodal logics in simple type theory | 2013-04-08 | Paper |
| MetiTarski: Past and Future | 2012-09-20 | Paper |
| Real Algebraic Strategies for MetiTarski Proofs | 2012-09-07 | Paper |
| Extending Sledgehammer with SMT Solvers | 2011-07-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086787 | 2011-03-30 | Paper |
| Multimodal and intuitionistic logics in simple type theory | 2010-12-14 | Paper |
| MetiTarski: An automatic theorem prover for real-valued special functions | 2010-05-26 | Paper |
| Applications of MetiTarski in the Verification of Control and Hybrid Systems | 2009-04-30 | Paper |
| Lightweight relevance filtering for machine-generated resolution problems | 2009-03-25 | Paper |
| MetiTarski: An Automatic Prover for the Elementary Functions | 2009-01-27 | Paper |
| The Isabelle Framework | 2008-12-04 | Paper |
| LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) | 2008-11-27 | Paper |
| Source-Level Proof Reconstruction for Interactive Theorem Proving | 2008-09-02 | Paper |
| The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF | 2008-06-19 | Paper |
| Extending a Resolution Prover for Inequalities on Elementary Functions | 2008-05-15 | Paper |
| Translating higher-order clauses to first-order clauses | 2008-02-18 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| Verifying the SET purchase protocols | 2007-01-30 | Paper |
| Automation for interactive proof: first prototype | 2006-10-25 | Paper |
| Theorem Proving in Higher Order Logics | 2006-07-06 | Paper |
| Mechanizing compositional reasoning for concurrent systems: some lessons | 2005-12-13 | Paper |
| Organizing numerical theories using axiomatic type classes | 2005-05-17 | Paper |
| The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf | 2004-11-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4809073 | 2004-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4411553 | 2003-07-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4411554 | 2003-07-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4790653 | 2003-02-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4786009 | 2002-12-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4786010 | 2002-12-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539594 | 2002-07-10 | Paper |
| Isabelle/HOL. A proof assistant for higher-order logic | 2002-06-12 | Paper |
| A simple formalization and proof for the mutilated chess board | 2001-06-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4520767 | 2001-02-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4946078 | 2001-01-11 | Paper |
| Mechanizing Nonstandard Real Analysis | 2000-09-25 | Paper |
| A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L | 2000-09-11 | Paper |
| Final coalgebras as greatest fixed points in ZF set theory | 2000-06-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4934138 | 2000-01-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4249889 | 1999-11-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364537 | 1999-03-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4217948 | 1998-11-11 | Paper |
| Mechanizing coinduction and corecursion in higher-order logic | 1997-12-14 | Paper |
| Mechanizing set theory. Cardinal arithmetic and the axiom of choice | 1997-08-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5687569 | 1996-12-16 | Paper |
| Set theory for verification. II: Induction and recursion | 1995-12-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4318835 | 1995-01-10 | Paper |
| Set theory for verification. I: From foundations to functions | 1994-12-11 | Paper |
| Isabelle. A generic theorem prover | 1994-08-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3972529 | 1992-06-25 | Paper |
| The foundation of a generic theorem prover | 1989-01-01 | Paper |
| Logic and Computation | 1987-01-01 | Paper |
| Constructing recursion operators in intuitionistic type theory | 1986-01-01 | Paper |
| Proving termination of normalization functions for conditional expressions | 1986-01-01 | Paper |
| Natural deduction as higher-order resolution | 1986-01-01 | Paper |
| Verifying the unification algorithm in LCF | 1985-01-01 | Paper |
| Lessons learned from LCF: A Survey of Natural Deduction Proofs | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3330551 | 1984-01-01 | Paper |
| A higher-order implementation of rewriting | 1983-01-01 | Paper |
