Related papers: Natural Deduction and the Isabelle Proof Assistant
We report a four-years experiment in teaching reasoning to undergraduate students, ranging from weak to gifted, using Gentzen-Prawitz's style natural deduction. We argue that this pedagogical approach is a good alternative to the use of…
The motivation for this paper comes out of our experience with teaching natural deduction (ND) and with the way this formal system is implemented by the \textsc{Coq} proof assistant, namely by means of so-called tactics, which are…
Theorem proving in natural mathematical language - the mixture of symbolic and natural language used by humans - plays a central role in mathematical advances and education, and tests aspects of reasoning that are core to intelligence. Yet…
We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem…
G\"odel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction…
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 present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good…
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an…
A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting several different logics. Isabelle has the…
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a…
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may…
Transformers have been shown to emulate logical deduction over natural language theories (logical rules expressed in natural language), reliably assigning true/false labels to candidate implications. However, their ability to generate…
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a computer can parse them and check them against the rules of a…
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized…
The purpose of this paper is to give an easy to understand with step-by-step explanation to allow interested people to fully appreciate the power of natural deduction for first-order logic. Natural deduction as a proof system can be used to…
A growing body of work studies how to answer a question or verify a claim by generating a natural language "proof": a chain of deductive inferences yielding the answer based on a set of premises. However, these methods can only make sound…
We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification…
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…
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 mathematical proof education, there remains a need for interventions that help students learn to write mathematical proofs. Research has shown that timely feedback can be very helpful to students learning new skills. While for many years…