Related papers: NaDeA: A Natural Deduction Assistant with a Formal…
Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate this process, we present smart_induct for Isabelle/HOL. Given…
In this paper, we propose the use of interactive theorem proving for explainable machine learning. After presenting our proposition, we illustrate it on the dedicated application of explaining security attacks using the Isabelle…
This book chapter establishes connections between the interactive proof tool Isabelle and classical tableau and resolution technology. Isabelle's classical reasoner is described and demonstrated by an extended case study: the Church-Rosser…
PyLog is a minimal experimental proof assistant based on linearised natural deduction for intuitionistic and classical first-order logic extended with a comprehension operator. PyLog is interesting as a tool to be used in conjunction with…
The Isabelle Archive of Formal Proofs has grown to a significant size in the past years. It makes up for an impressive body of research, which enables a number of statistical approaches to various aspects in theorem proving, and has not yet…
This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle's existing logical framework infrastructure to implement essential…
In order to help students learn how to write mathematical proofs, we adapt the Coq proof assistant into an educational tool we call Waterproof. Like with other interactive theorem provers, students write out their proofs inside the software…
In parallel to the ever-growing usage of mechanized proofs in diverse areas of mathematics and computer science, proof assistants are used more and more for education. This paper surveys previous work related to the use of proof assistants…
We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemini CLI, and it is designed to run on consumer grade…
We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…
Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based access control) and to enable reproducibility and accountability (e.g. provenance in scientific programming).…
Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor…
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library…
Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a novel…
Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different tools are being increasingly used in…
It has recently become feasible to run personal digital assistants on phones and other personal devices. In this paper we describe a design for a natural language understanding system that runs on device. In comparison to a server-based…
In settings from fact-checking to question answering, we frequently want to know whether a collection of evidence (premises) entails a hypothesis. Existing methods primarily focus on the end-to-end discriminative version of this task, but…
We report on several scenarios of using automated theorem proving software in university education. In particular, we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial…
Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code base is annotated with a function contract specifying its…
Tackling Natural Language Inference with a logic-based method is becoming less and less common. While this might have been counterintuitive several decades ago, nowadays it seems pretty obvious. The main reasons for such a conception are…