Search
Search Results
-
Linear Resources in Isabelle/HOL
We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of...
-
Mechanising Gödel–Löb Provability Logic in HOL Light
We introduce our implementation in HOL Light of the metatheory for Gödel–Löb provability logic (GL), covering soundness and completeness w.r.t....
-
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search...
-
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL
We present a formalization of several fundamental notions and results from Quantum Information theory in the proof assistant Isabelle/HOL, including...
-
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL
We have formalised Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions, two major results in extremal graph theory and...
-
Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL
Special relativity is a cornerstone of modern physical theory. While a standard coordinate model is well known and widely taught today, multiple...
-
ULKB Logic: A HOL-Based Framework for Reasoning over Knowledge Graphs
ULKB Logic is an open-source framework written in Python for reasoning over knowledge graphs. It provides an interactive theorem prover-like...
-
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Satisfiability modulo theories (SMT) solvers are widely used to ensure the correctness of safety- and security-critical applications. Therefore,...
-
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL
Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style...
-
Verifying Feedforward Neural Networks for Classification in Isabelle/HOL
Neural networks are being used successfully to solve classification problems, e.g., for detecting objects in images. It is well known that neural...
-
Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL
This paper addresses the formal verification of reconfigurable discrete event systems (RDESs) using Isabelle/HOL proof assistant. A reconfigurable...
-
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a...
-
An Isabelle/HOL Formalization of the SCL(FOL) Calculus
We present an Isabelle/HOL formalization of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal...
-
Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem
Free groups are central to group theory, and are ubiquitous across many branches of mathematics, including algebra, topology and geometry. An...
-
On the Formalization of the Heat Conduction Problem in HOL
Partial Differential Equations (PDEs) are widely used for modeling the physical phenomena and analyzing the dynamical behavior of many engineering...
-
Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL
The verification framework PPV (Probabilistic Program Verification) verifies functional probabilistic programs supporting higher-order functions,...
-
Dyadic Deontic Logic in HOL: Faithful Embedding and Meta-Theoretical Experiments
A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. The embedding is proven...
-
A Verified Implementation of B \(^+\) -Trees in Isabelle/HOL
In this paper we present the verification of an imperative implementation of the ubiquitous B...
-
Certified Quantum Computation in Isabelle/HOL
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant...
-
Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started
This is an account of a mathematician’s first experiences with the proof assistant (interactive theorem prover) Isabelle/HOL, including a discussion...
