A Formal Proof of Cauchy’s Residue Theorem

article published in 2016

A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS

A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle

A formalised theorem in the partition calculus

scientific article published in 2024

A higher-order implementation of rewriting

A modular, efficient formalisation of real algebraic numbers

article

A semantics-directed compiler generator

Accountability protocols

An Isabelle/HOL Formalisation of Green’s Theorem

An overview of the verification of SET

Applications of MetiTarski in the Verification of Control and Hybrid Systems

Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition ⬇️

article

Automated theorem proving for special functions

Automation for interactive proof: First prototype

Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions

Computational logic: its origins and applications.

scientific article published on 28 February 2018

Constructing recursion operators in intuitionistic type theory

Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL

Defining functions on equivalence classes

Erratum to “Automation for interactive proof: First prototype” [Inform. and Comput. 204 (2006) 1575–1596]

scholarly article published in Information and Computation

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL

scientific article published on 03 April 2019

Experiments on Supporting Interactive Proof Using Resolution

Extending Sledgehammer with SMT Solvers

Extending Sledgehammer with SMT Solvers

Formal Verification of Cardholder Registration in SET

Formal Verification of Transcendental Fixed and Floating Point Algorithms using an Automatic Theorem Prover

scientific article published in 2022

Formal verification of analog designs using MetiTarski

article

Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

scientific article published in 2022

Introduction to Milestones in Interactive Theorem Proving

Is the Verification Problem for Cryptographic Protocols Solved?

Isabelle: The next seven hundred theorem provers

Kerberos Version IV: Inductive analysis of the secrecy goals

LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)

LEO-II and Satallax on the Sledgehammer test bench

Lightweight relevance filtering for machine-generated resolution problems

Logic and Computation

Machine Learning for First-Order Theorem Proving

scholarly article by James P. Bridge et al published 22 February 2014 in Journal of Automated Reasoning

Mechanical Proofs about a Non-repudiation Protocol

Mechanizing Nonstandard Real Analysis

article published in 2000

Mechanizing UNITY in Isabelle

Mechanizing a theory of program composition for UNITY

article

Mechanizing compositional reasoning for concurrent systems: some lessons

article

MetiTarski: An Automatic Prover for the Elementary Functions

MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions

scientific article (publication date: 18 August 2009)

MetiTarski: Past and Future

Michael John Caldwell Gordon. 28 February 1948—22 August 2017

scientific article published on 12 September 2018

Natural deduction as higher-order resolution

Organizing Numerical Theories Using Axiomatic Type Classes

Preface

Proofs and Reconstructions

Quantified Multimodal Logics in Simple Type Theory

Real Algebraic Strategies for MetiTarski Proofs

scholarly article by Grant Olney Passmore et al published 2012 in Lecture Notes in Computer Science

Relations between secrets: two formal analyses of the Yahalom protocol

scientific article published in 2001

Set theory for verification. II: Induction and recursion

Set theory for verification: I. From foundations to functions

The Descent of BAN

The Higher-Order Prover Leo-II

scientific article published on 22 September 2015

The Reflection Theorem: A Study in Meta-theoretic Reasoning

article

The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf

scientific article published in 2003

The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF

The foundation of a generic theorem prover

The inductive approach to verifying cryptographic protocols

scientific article published in 1998

Tool Support for Logics of Programs

Translating Higher-Order Clauses to First-Order Clauses

article by Jia Meng & Lawrence Paulson published 15 September 2007 in Journal of Automated Reasoning

Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases ⬇️

article

Verifying Hybrid Systems Involving Transcendental Functions

Verifying multicast-based security protocols using the inductive method

Verifying multicast-based security protocols using the inductive method

Verifying the SET Purchase Protocols

Verifying the unification algorithm in LCF