Related papers: Natural Deduction and the Isabelle Proof Assistant
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,…
We describe a strategy-based approach to teaching natural deduction using a notation that emphasises the order in which deductions are constructed, together with a {\LaTeX} package and Java app to aid in the production of teaching resources…
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…
Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search,…
Elfe is an interactive system for teaching basic proof methods in discrete mathematics. The user inputs a mathematical text written in fair English which is converted to a special data-structure of first-order formulas. Certain proof…
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…
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 introduce real induction, a proof technique analogous to mathematical induction but applicable to statements indexed by an interval on the real line. More generally we give an inductive principle applicable in any Dedekind complete…
Software tools of Automated Reasoning are too sophisticated for general use in mathematics education and respective reasoning, while Lucas-Interpretation provides a general concept for integrating such tools into educational software with…
Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof…
This is an overview of the Isabelle technology behind the Archive of Formal Proofs (AFP). Interactive development and quasi-interactive build jobs impose significant demands of scalability on the logic (usually Isabelle/HOL), on Isabelle/ML…
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…
Automatic verification deals with the validation by means of computers of correctness certificates. The related tools, usually called proof assistants or interactive provers, provide an interactive environment for the creation of formal…
The application of automatic theorem provers to discharge proof obligations is necessary to apply formal methods in an efficient manner. Tools supporting formal methods, such as Atelier~B, generate proof obligations fully automatically.…
Teaching precise mathematical reasoning can be very hard. It is very easy for a student to make a subtle mistake in a proof which invalidates it, but it is often hard for the teacher to pinpoint and explain the problem in the (often…
Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification…
Understanding geometric relationships with little mathematical knowledge can be challenging for today's students and teachers. A new toolset is introduced that is able to create a proof without words by combining the benefits of the…
We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasoning tools. Theoretically, interactive protocols exist for all…
We report about significant enhancements of the complex algebraic geometry theorem proving subsystem in GeoGebra for automated proofs in Euclidean geometry, concerning the extension of numerous GeoGebra tools with proof capabilities. As a…
Isabelle/PIDE is the current Prover IDE technology for Isabelle. It has been developed in ML and Scala in the past 4-5 years for this particular proof assistant, but with an open mind towards other systems. PIDE is based on an asynchronous…