相关论文: Conversion of HOL Light proofs into Metamath

The present dissertation introduces the research project on HOLMS (\textbf{HOL} Light Library for \textbf{M}odal \textbf{S}ystems), a growing modular framework for modal reasoning within the HOL Light proof assistant. To provide an…

We observe today a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to co-operate because they do not…

Transform methods, like Laplace and Fourier, are frequently used for analyzing the dynamical behaviour of engineering and physical systems, based on their transfer function, and frequency response or the solutions of their corresponding…

LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's…

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on…

We introduce our implementation in HOL Light of the metatheory for G\"odel-L\"ob provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The…

New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In…

The Common HOL project aims to facilitate porting source code and proofs between members of the HOL family of theorem provers. At the heart of the project is the Common HOL Platform, which defines a standard HOL theory and API that aims to…

Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such…

Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate the proofs of a family of HOL proof assistants to Dedukti. The…

We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. ${\rm CTT}_{\rm qe}$ is a version of Church's type…

This work presents a formalized proof of modal completeness for G\"odel-L\"ob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices…

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…

Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they have, and are in turn formalized, are the same. For the…

We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns…

Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof assistant and an adaptation of the HOLyHammer system that…

In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 theorem prover, with some improvements and new theorems.…

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…

This report describes three particular technological advances in formal proofs. The HOL Light proof assistant will be used to illustrate the design of a highly reliable system. Today, proof assistants can verify large bodies of advanced…

An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant…