Related papers: On Exams with the Isabelle Proof Assistant
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of…
The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although,…
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…
Undergraduate students of artificial intelligence often struggle with representing knowledge as logical sentences. This is a skill that seems to require extensive practice to obtain, suggesting a teaching strategy that involves the…
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…
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In…
Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof…
We present a new software tool for teaching logic based on natural deduction. Its proof system is formalized in the proof assistant Isabelle such that its definition is very precise. Soundness of the formalization has been proved in…
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and…
We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main…
Formal verification of cyber-physical and robotic systems requires that we can accurately model physical quantities that exist in the real-world. The use of explicit units in such quantities can allow a higher degree of rigour, since we can…
We report on our journey to develop ProofBuddy, a web application that is powered by a server-side instance of the proof assistant Isabelle, for the teaching and learning of proofs and proving. The journey started from an attempt to use…
We describe our Natural Deduction Assistant (NaDeA) and the interfaces between the Isabelle proof assistant and NaDeA. In particular, we explain how NaDeA, using a generated prover that has been verified in Isabelle, provides feedback to…
On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we…
Grading of examination papers is a hectic, time-labor intensive task and is often subjected to inefficiency and bias in checking. This research project is a primitive experiment in the automation of grading of theoretical answers written in…
The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant.…
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance…
A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first authors universal logical reasoning…
We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low…
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…