| Publication | Date of Publication | Type |
|---|
| Formalising half of a graduate textbook on number theory (short paper) | 2026-02-10 | Paper |
Mathematical proof between generations
Notices of the American Mathematical Society | 2024-09-26 | Paper |
| Formalising Fisher's inequality: formal linear algebraic proof techniques in combinatorics | 2024-07-15 | Paper |
Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
Lecture Notes in Computer Science | 2024-02-28 | Paper |
A concrete final coalgebra theorem for ZF set theory
Lecture Notes in Computer Science | 2023-12-08 | Paper |
A formalised theorem in the partition calculus
Annals of Pure and Applied Logic | 2023-10-12 | Paper |
Formalising Mathematics in Simple Type Theory
Synthese Library | 2023-09-20 | Paper |
Formalising Mathematics in Simple Type Theory
Synthese Library | 2023-09-20 | Paper |
Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
Formal Aspects of Computing | 2023-08-31 | Paper |
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
Journal of Automated Reasoning | 2023-06-14 | Paper |
Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis
Lecture Notes in Computer Science | 2023-06-02 | Paper |
| Bayesian ranking for strategy scheduling in automated theorem provers | 2022-12-07 | Paper |
Algebraically Closed Fields in Isabelle/HOL
Automated Reasoning | 2022-11-09 | Paper |
Formalizing ordinal partition relations using Isabelle/HOL
Experimental Mathematics | 2022-08-03 | Paper |
Simple type theory is not too simple: Grothendieck's schemes without dependent types
Experimental Mathematics | 2022-08-03 | Paper |
Irrationality and transcendence criteria for infinite series in Isabelle/HOL
Experimental Mathematics | 2022-08-03 | Paper |
A modular first formalisation of combinatorial design theory
(available as arXiv preprint) | 2022-04-22 | Paper |
ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
The Bulletin of Symbolic Logic | 2022-03-01 | Paper |
Formalising Ordinal Partition Relations Using Isabelle/HOL
(available as arXiv preprint) | 2020-11-26 | Paper |
Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
Journal of Automated Reasoning | 2020-03-03 | Paper |
A fixedpoint approach to implementing (co)inductive definitions
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
From LCF to Isabelle/HOL
Formal Aspects of Computing | 2019-12-18 | Paper |
Using machine learning to improve cylindrical algebraic decomposition
Mathematics in Computer Science | 2019-11-27 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
An Isabelle/HOL formalisation of Green's theorem
Journal of Automated Reasoning | 2019-09-02 | Paper |
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
Journal of Automated Reasoning | 2019-02-15 | Paper |
Computational logic: its origins and applications
Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences | 2018-12-04 | Paper |
Defining functions on equivalence classes
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Mechanizing UNITY in Isabelle
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Proofs and reconstructions
Frontiers of Combining Systems | 2017-02-27 | Paper |
A formal proof of Cauchy's residue theorem
Interactive Theorem Proving | 2016-10-27 | Paper |
An Isabelle/HOL formalisation of Green's theorem
Interactive Theorem Proving | 2016-10-27 | Paper |
Automated theorem proving for special functions: the next phase
Proceedings of the 2014 Symposium on Symbolic-Numeric Computation | 2016-09-29 | Paper |
A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
Journal of Automated Reasoning | 2016-05-26 | Paper |
The higher-order prover \textsc{Leo}-II
Journal of Automated Reasoning | 2016-05-26 | Paper |
A formalisation of finite automata using hereditarily finite sets
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Extending Sledgehammer with SMT solvers
Journal of Automated Reasoning | 2015-06-23 | Paper |
Machine learning for first-order theorem proving
Journal of Automated Reasoning | 2015-06-23 | Paper |
A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
The Review of Symbolic Logic | 2015-01-21 | Paper |
Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
Lecture Notes in Computer Science | 2014-08-07 | Paper |
MetiTarski's menagerie of cooperating systems
Frontiers of Combining Systems | 2013-09-20 | Paper |
Case splitting in an automatic theorem prover for real-valued special functions
Journal of Automated Reasoning | 2013-07-05 | Paper |
LEO-II and Satallax on the Sledgehammer test bench
Journal of Applied Logic | 2013-05-02 | Paper |
Quantified multimodal logics in simple type theory
Logica Universalis | 2013-04-08 | Paper |
MetiTarski: past and future
Interactive Theorem Proving | 2012-09-20 | Paper |
Real Algebraic Strategies for MetiTarski Proofs
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Extending Sledgehammer with SMT solvers
Lecture Notes in Computer Science | 2011-07-29 | Paper |
| Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II} | 2011-03-30 | Paper |
Multimodal and intuitionistic logics in simple type theory
Logic Journal of the IGPL | 2010-12-14 | Paper |
MetiTarski: An automatic theorem prover for real-valued special functions
Journal of Automated Reasoning | 2010-05-26 | Paper |
Applications of MetiTarski in the Verification of Control and Hybrid Systems
Hybrid Systems: Computation and Control | 2009-04-30 | Paper |
Lightweight relevance filtering for machine-generated resolution problems
Journal of Applied Logic | 2009-03-25 | Paper |
MetiTarski: An Automatic Prover for the Elementary Functions
Lecture Notes in Computer Science | 2009-01-27 | Paper |
The Isabelle Framework
Lecture Notes in Computer Science | 2008-12-04 | Paper |
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
Automated Reasoning | 2008-11-27 | Paper |
Source-Level Proof Reconstruction for Interactive Theorem Proving
Lecture Notes in Computer Science | 2008-09-02 | Paper |
The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
Logic and Theory of Algorithms | 2008-06-19 | Paper |
Extending a Resolution Prover for Inequalities on Elementary Functions
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
Translating higher-order clauses to first-order clauses
Journal of Automated Reasoning | 2008-02-18 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Verifying the SET purchase protocols
Journal of Automated Reasoning | 2007-01-30 | Paper |
Automation for interactive proof: first prototype
Information and Computation | 2006-10-25 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Mechanizing compositional reasoning for concurrent systems: some lessons
Formal Aspects of Computing | 2005-12-13 | Paper |
Organizing numerical theories using axiomatic type classes
Journal of Automated Reasoning | 2005-05-17 | Paper |
The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
LMS Journal of Computation and Mathematics | 2004-11-18 | Paper |
| scientific article; zbMATH DE number 2090314 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 1947524 (Why is no real title available?) | 2003-07-09 | Paper |
| scientific article; zbMATH DE number 1947525 (Why is no real title available?) | 2003-07-09 | Paper |
| scientific article; zbMATH DE number 1863379 (Why is no real title available?) | 2003-02-04 | Paper |
| scientific article; zbMATH DE number 1844576 (Why is no real title available?) | 2002-12-12 | Paper |
| scientific article; zbMATH DE number 1844577 (Why is no real title available?) | 2002-12-12 | Paper |
| scientific article; zbMATH DE number 1765658 (Why is no real title available?) | 2002-07-10 | Paper |
Isabelle/HOL. A proof assistant for higher-order logic
Lecture Notes in Computer Science | 2002-06-12 | Paper |
A simple formalization and proof for the multilated chess board
Logic Journal of the IGPL | 2001-06-26 | Paper |
| scientific article; zbMATH DE number 1543300 (Why is no real title available?) | 2001-02-27 | Paper |
| scientific article; zbMATH DE number 1421054 (Why is no real title available?) | 2001-01-11 | Paper |
Mechanizing Nonstandard Real Analysis
LMS Journal of Computation and Mathematics | 2000-09-25 | Paper |
A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
Journal of Automated Reasoning | 2000-09-11 | Paper |
Final coalgebras as greatest fixed points in ZF set theory
Mathematical Structures in Computer Science | 2000-06-13 | Paper |
| scientific article; zbMATH DE number 1389645 (Why is no real title available?) | 2000-01-17 | Paper |
| scientific article; zbMATH DE number 1303336 (Why is no real title available?) | 1999-11-16 | Paper |
| scientific article; zbMATH DE number 1088221 (Why is no real title available?) | 1999-03-22 | Paper |
| scientific article; zbMATH DE number 1222424 (Why is no real title available?) | 1998-11-11 | Paper |
Mechanizing coinduction and corecursion in higher-order logic
Journal Of Logic And Computation | 1997-12-14 | Paper |
Mechanizing set theory. Cardinal arithmetic and the axiom of choice
Journal of Automated Reasoning | 1997-08-03 | Paper |
| scientific article; zbMATH DE number 958048 (Why is no real title available?) | 1996-12-16 | Paper |
Set theory for verification. II: Induction and recursion
Journal of Automated Reasoning | 1995-12-20 | Paper |
| scientific article; zbMATH DE number 709076 (Why is no real title available?) | 1995-01-10 | Paper |
Set theory for verification. I: From foundations to functions
Journal of Automated Reasoning | 1994-12-11 | Paper |
Isabelle. A generic theorem prover
Lecture Notes in Computer Science | 1994-08-22 | Paper |
| scientific article; zbMATH DE number 15883 (Why is no real title available?) | 1992-06-25 | Paper |
The foundation of a generic theorem prover
Journal of Automated Reasoning | 1989-01-01 | Paper |
| Logic and Computation | 1987-01-01 | Paper |
Constructing recursion operators in intuitionistic type theory
Journal of Symbolic Computation | 1986-01-01 | Paper |
Natural deduction as higher-order resolution
The Journal of Logic Programming | 1986-01-01 | Paper |
Proving termination of normalization functions for conditional expressions
Journal of Automated Reasoning | 1986-01-01 | Paper |
Verifying the unification algorithm in LCF
Science of Computer Programming | 1985-01-01 | Paper |
Lessons learned from LCF: A Survey of Natural Deduction Proofs
The Computer Journal | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3862480 (Why is no real title available?) | 1984-01-01 | Paper |
A higher-order implementation of rewriting
Science of Computer Programming | 1983-01-01 | Paper |
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
(available as arXiv preprint) | N/A | Paper |
Formal Probabilistic Methods for Combinatorial Structures using the Lov\'asz Local Lemma
(available as arXiv preprint) | N/A | Paper |
