Related papers: Matching concepts across HOL libraries
Interactive theorem provers, like Isabelle/HOL, Coq and Lean, have expressive languages that allow the formalization of general mathematical objects and proofs. In this context, an important goal is to reduce the time and effort needed to…
HOL(y)Hammer is an online AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system. The service allows its users to upload and automatically process an arbitrary formal development (project) based on…
Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by…
We propose a formalization of generic algorithms that includes analog algorithms. This is achieved by reformulating and extending the framework of abstract state machines to include continuous-time models of computation. We prove that every…
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof…
Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most time and effort that is invested in proving is actually…
We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics…
We present a formalization of modern SAT solvers and their properties in a form of abstract state transition systems. SAT solving procedures are described as transition relations over states that represent the values of the solver's global…
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to…
We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Chapters 2--8), from topological spaces through dimension…
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This involves proving statements in any logic using intuitive…
Similarity measures are fundamental tools for quantifying the alignment between artificial and biological systems. However, the diversity of similarity measures and their varied naming and implementation conventions makes it challenging to…
A classification, according to invariant theory, of non-constant invariant Abel ODEs known as solvable and found in the literature is presented. A set of new integrable classes depending on one or no parameters, derived from the analysis of…
This paper presents a formalisation of pGCL in Isabelle/HOL. Using a shallow embedding, we demonstrate close integration with existing automation support. We demonstrate the facility with which the model can be extended to incorporate…
The problems of estimating the similarity index of inhomogeneous scientific publications containing equations and formulas are discussed for the first time. It is shown that the presence of equations and formulas (as well as figures,…
A central problem in proof-theory is that of finding criteria for identity of proofs, that is, for when two distinct formal derivations can be taken as denoting the same logical argument. In the literature one finds criteria which are…
Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annotations for rank-one polymorphic $\lambda$-calculus terms, as…
We present a complete formalization in Isabelle/HOL of the object part of an equivalence between L-mosaics and bounded join-semilattices, employing an AI-assisted methodology that integrates large language models as reasoning assistants…
Linear algebra is a major field of numerical computation and is widely applied. Most linear algebra libraries (in most programming languages) do not statically guarantee consistency of the dimensions of vectors and matrices, causing runtime…
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP's intermediate language, called BIL and integrate it with…