JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants

2001 ◽  
pp. 421-426 ◽  
Author(s):  
Stephan Schmitt ◽  
Lori Lorigo ◽  
Christoph Kreitz ◽  
Aleksey Nogin
Keyword(s):  
Theorem Proving ◽  
Proof Assistants ◽  
Interactive Proof

scholarly journals Competitive Proving for Fun

10.29007/ktx8 ◽  
2019 ◽  
Author(s):  
Maximilian Paul Louis Haslbeck ◽  
Simon Wimmer
Keyword(s):  
Theorem Proving ◽  
System Architecture ◽  
Large Scale ◽  
Research Field ◽  
Proof Assistant ◽  
Proof Assistants ◽  
Prototype Implementation ◽  
New Generation

We propose a system for large-scale theorem proving contests. We hope that such contests could spark interest in the research field, attract a new generation of theorem proving savants, and foster competition among proof assistants. For the proof assistant Isabelle, we construct and evaluate two iterations of a prototype implementation of our proposed system architecture.

Interactive proof-search for equational reasoning

2020 ◽  
Author(s):  
Favio E Miranda-Perea ◽  
Lourdes del Carmen González Huesca ◽  
P Selene Linares-Arévalo
Keyword(s):  
Functional Programming ◽  
Formal System ◽  
Deductive System ◽  
Proof Assistants ◽  
Interactive Proof ◽  
Equational Reasoning ◽  
Mathematical Proofs ◽  
Proof Search ◽  
The Common ◽  
Definition Of

Abstract Equational reasoning arises in many areas of mathematics and computer science. It is a cornerstone of algebraic reasoning and results essential in tasks of specification and verification in functional programming, where a program is mainly a set of equations. The usual manipulation of identities while conducting informal proofs obviates many intermediate steps that are neccesary while developing them using a formal system, such as the equationally complete Birkhoff calculus ${\mathcal{B}}$. This deductive system does not fit in the common manner of doing mathematical proofs, and it is not compatible with the mechanisms of proof assistants. The aim of this work is to provide a deductive system ${\mathcal{B}}^{\textrm{GOAL}}$ for equality, equivalent to ${\mathcal{B}}$ but suitable for constructing equational proofs in a backward fashion. This feature makes it adequate for interactive proof-search in the approach of proof assistants. This will be achieved by turning ${\mathcal{B}}^{\textrm{GOAL}}$ into a transition system of formal tactics in the style of Edinburgh LCF, such transformation allows us to give a direct formal definition of backward proof in equational logic.

scholarly journals Going Polymorphic - TH1 Reasoning for Leo-III

10.29007/jgkw ◽  
2018 ◽  
Author(s):  
Alexander Steen ◽  
Max Wisniewski ◽  
Christoph Benzmüller
Keyword(s):  
Type Systems ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Proof Assistants ◽  
Interactive Proof ◽  
Higher Order Logic ◽  
Theorem Provers ◽  
Reasoning System ◽  
Automated Theorem Prover

While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and therefore do not allow such flexibility. In this paper, we present modifications to the higher-order automated theorem prover Leo-III for turning it into a reasoning system for rank-1 polymorphic HOL.To that end, a polymorphic version of HOL and a suitable paramodulation-based calculus are sketched. The implementation is evaluated using a set of polymorphic TPTP THF problems.

scholarly journals Zen and the art of formalisation

2011 ◽  
Vol 21 (4) ◽  
pp. 679-682 ◽  
Author(s):  
ANDREA ASPERTI ◽  
JEREMY AVIGAD
Keyword(s):  
Theorem Proving ◽  
Interactive Theorem Proving ◽  
Professor Emeritus ◽  
Proof Assistants ◽  
De Bruijn Graphs ◽  
University Of Technology ◽  
De Bruijn Sequences ◽  
Basic Technology ◽  
De Bruijn ◽  
The Many

N. G. de Bruijn, now professor emeritus of the Eindhoven University of Technology, was a pioneer in the field of interactive theorem proving. From 1967 to the end of the 1970's, his work on the Automath system introduced the architecture that is common to most of today's proof assistants, and much of the basic technology. But de Bruijn was a mathematician first and foremost, as evidenced by the many mathematical notions and results that bear his name, among them de Bruijn sequences, de Bruijn graphs, the de Bruijn–Newman constant, and the de Bruijn–Erdös theorem. The quotation above is thus interesting not because it is a reflection on his expertise in formal verification, but, rather, of his convictions as a working mathematician.

scholarly journals Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’

2015 ◽  
Vol 373 (2039) ◽  
pp. 20140234 ◽  
Author(s):  
M. J. C. Gordon
Keyword(s):  
Computer Science ◽  
Theorem Proving ◽  
Royal Society ◽  
Mathematical Reasoning ◽  
Computer Assisted ◽  
Proof Assistants ◽  
Rigorous Proof ◽  
Proof Construction ◽  
Practical Tool ◽  
350Th Anniversary

Robin Milner's paper, ‘The use of machines to assist in rigorous proof’, introduces methods for automating mathematical reasoning that are a milestone in the development of computer-assisted theorem proving. His ideas, particularly his theory of tactics, revolutionized the architecture of proof assistants. His methodology for automating rigorous proof soundly, particularly his theory of type polymorphism in programing, led to major contributions to the theory and design of programing languages. His citation for the 1991 ACM A.M. Turing award, the most prestigious award in computer science, credits him with, among other achievements, ‘probably the first theoretically based yet practical tool for machine assisted proof construction’. This commentary was written to celebrate the 350th anniversary of the journal Philosophical Transactions of the Royal Society .

scholarly journals A light-weight integration of automated and interactive theorem proving

2014 ◽  
Vol 26 (1) ◽  
pp. 129-153 ◽  
Author(s):  
KARIM KANSO ◽  
ANTON SETZER
Keyword(s):  
Theorem Proving ◽  
Interactive Theorem Proving ◽  
Theorem Prover ◽  
Finite Domain ◽  
Infinite Domain ◽  
Interactive Proof ◽  
Domain Experts ◽  
Automated Theorem Prover ◽  
Efficient Verification

In this paper, aimed at dependently typed programmers, we present a novel connection between automated and interactive theorem proving paradigms. The novelty is that the connection offers a better trade-off between usability, efficiency and soundness when compared to existing techniques. This technique allows for a powerful interactive proof framework that facilitates efficient verification of finite domain theorems and guided construction of the proof of infinite domain theorems. Such situations typically occur with industrial verification. As a case study, an embedding of SAT and CTL model checking is presented, both of which have been implemented for the dependently typed proof assistant Agda.Finally, an example of a real world railway control system is presented, and shown using our proof framework to be safe with respect to an abstract model of trains not colliding or derailing. We demonstrate how to formulate safety directly and show using interactive theorem proving that signalling principles imply safety. Therefore, a proof by an automated theorem prover that the signalling principles hold for a concrete system implies the overall safety. Therefore, instead of the need for domain experts to validate that the signalling principles imply safety they only need to make sure that the safety is formulated correctly. Therefore, some of the validation is replaced by verification using interactive theorem proving.

scholarly journals Experiences from Exporting Major Proof Assistant Libraries

2021 ◽  
Author(s):  
Michael Kohlhase ◽  
Florian Rabe
Keyword(s):  
Theorem Proving ◽  
Proof Assistant ◽  
Proof Assistants ◽  
Social Challenges ◽  
Future System ◽  
Hol Light ◽  
System Interoperability

AbstractThe interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution, and our experiences will prove valuable to others undertaking such efforts.

Sign in / Sign up

Export Citation Format

Share Document