Related papers: Formalization of PAL$\cdot$S5 in Proof Assistant
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic.…
We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach is grounded in two key insights. First, informal proofs tend…
Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most…
In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between…
Formal reasoning and automated theorem proving constitute a challenging subfield of machine learning, in which machines are tasked with proving mathematical theorems using formal languages like Lean. A formal verification system can check…
In this note, a formal transition system model called LTPAL to extract knowledge in a classification process is suggested. The model combines the Public Announcement Logic (PAL) and the Linear Temporal Logic (LTL). In the model, first, we…
In 1933, G\"odel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay's Completeness Theorem. The other was based on the modal logic S4 and led to Artemov's…
Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER…
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an…
Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expertise. While Large Language Models (LLMs) have shown promise…
We use a mechanized verification system, PVS, to examine the argument from Anselm's Proslogion Chapter III, the so-called "Modal Ontological Argument." We consider several published formalizations for the argument and show they are all…
Proof assistants are computer softwares that allow us to write mathematical proofs so as to assess their correctness. In November 2021, I started the project of checking the simplicity of the alternating groups within the Lean theorem…
We propose a synthesis of the two proof styles of interactive theorem proving: the procedural style (where proofs are scripts of commands, like in Coq) and the declarative style (where proofs are texts in a controlled natural language, like…
We present three projects concerned with applications of proof assistants in the area of programming language theory and mathematics. The first project is about a certified compilation technique for a domain-specific programming language…
Proof engineering is notoriously labor-intensive: proofs that are straightforward on paper often require lengthy scripts in theorem provers. Recent advances in large language models (LLMs) create new opportunities for proof automation:…
This paper presents the Soda language for verifying multi-agent systems. Soda is a high-level functional and object-oriented language that supports the compilation of its code not only to Scala, a strongly statically typed high-level…
We present a general framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In our framework, the number of agents or the amount of certain…
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic.…
We propose a multi-agent epistemic logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents, and in the order in which they were sent. Additional to epistemic modalities the…
Formal theorem proving with TLA+ provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language models have shown promise in automating proofs for tactic-based…