scholarly journals Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs

10.29007/zbdb ◽  
2018 ◽  
Author(s):  
Steffen Juilf Smolka ◽  
Jasmin Christian Blanchette
Keyword(s):  
Companion Paper ◽  
Proof Assistant ◽  
Theorem Provers ◽  
Automatic Theorem Provers ◽  
Proof Methods ◽  
The Right ◽  
Automatic Theorem

Sledgehammer integrates external automatic theorem provers (ATPs) in the Isabelle/HOL proof assistant. To guard against bugs, ATP proofs must be reconstructed in Isabelle. Reconstructing complex proofs involves translating them to detailed Isabelle proof texts, using suitable proof methods to justify the inferences. This has been attempted before with little success, but we have addressed the main issues: Sledgehammer now transforms the proofs by contradiction into direct proofs (as described in a companion paper); it reconstructs skolemization inferences; it provides the right amount of type annotations to ensure formulas are parsed correctly without overwhelming them with types; and it iteratively tests and compresses the output, resulting in simpler and faster proofs.

scholarly journals Making Automatic Theorem Provers more Versatile

10.29007/n6j7 ◽  
2018 ◽  
Author(s):  
Simon Cruanes
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Research Directions ◽  
First Order ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.

Seventy-five problems for testing automatic theorem provers

1986 ◽  
Vol 2 (2) ◽  
pp. 191-216 ◽  
Author(s):  
Francis Jeffry Pelletier
Keyword(s):  
Theorem Provers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

A New Algebraic Tool for Automatic Theorem Provers

2004 ◽  
Vol 42 (4) ◽  
pp. 369-398 ◽  
Author(s):  
P. Cordero ◽  
G. Gutiérrez ◽  
J. Martínez ◽  
I.P. de Guzmán
Keyword(s):  
Theorem Provers ◽  
Automatic Theorem Provers ◽  
Algebraic Tool ◽  
Automatic Theorem

scholarly journals Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers

10.29007/36dt ◽  
2018 ◽  
Author(s):  
Lawrence C. Paulson ◽  
Jasmin Christian Blanchette
Keyword(s):  
Years Of Experience ◽  
Interactive Proof ◽  
Theorem Provers ◽  
Proof Construction ◽  
Interactive Theorem Provers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.

scholarly journals Integration of Automatic Theorem Provers in Event-B Patterns

2013 ◽  
Vol 4 (1) ◽  
pp. 29-42
Author(s):  
Eman Elsayed ◽  
Gaber El-Sharawy ◽  
Enas El-Sharawy
Keyword(s):  
Theorem Provers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

Tableaux Versus Resolution a Comparison

1993 ◽  
Vol 18 (2-4) ◽  
pp. 109-127
Author(s):  
W.M.J. Ophelders ◽  
H.C.M. De Swart
Keyword(s):  
Theorem Prover ◽  
Full Description ◽  
Test Results ◽  
Theorem Provers ◽  
Automatic Theorem Provers ◽  
Automated Theorem Prover ◽  
Main Ideas ◽  
Automatic Theorem

In [13] we have presented the ideas underlying an automated theorem prover based on tableaux extended with unification under restrictions. In [6] a full description of an implementation of this theorem prover in PROLOG is given. In this paper we first shortly repeat the main ideas, referring to [13] for more details. Next we present the test results of our theorem prover mainly with respect to Pelletier’s 75 problems for testing automatic theorem provers ([7]). We also give a comparison of our results with the results obtained by the resolution-based theorem provers PCPROVE and OTTER and by the tableau-based theorem provers of M. Fitting and S. Reeves. Short discussions of these theorem provers accompany the test results. For more elaborate discussions the reader is referred to [6].

scholarly journals Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers

10.29007/tnfd ◽  
2018 ◽  
Author(s):  
Lawrence Paulson
Keyword(s):  
Years Of Experience ◽  
Interactive Proof ◽  
Theorem Provers ◽  
Proof Construction ◽  
Interactive Theorem Provers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.

scholarly journals My Life with an Automatic Theorem Prover

10.29007/5b7w ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette
Keyword(s):  
Third Party ◽  
Theorem Prover ◽  
Theorem Provers ◽  
Automatic Theorem Provers ◽  
Future Work ◽  
Automatic Theorem

Sledgehammer integrates third-party automatic theorem provers in the proofassistant Isabelle/HOL. In the seven years since its first release in 2007, ithas grown to become an essential part of most Isabelle users' workflow. Althougha lot of work has gone into tuning the system, the main reason forSledgehammer's success is the impressive power of the external provers,especially E, SPASS, Vampire, and Z3. In this paper, I reviewVampire's strengths and weaknesses in this context and propose a fewdirections for future work.

Shortening of Proof Length is Elusive for Theorem Provers

2020 ◽  
Vol 30 (04) ◽  
pp. 2050013
Author(s):  
Santiago Hernández-Orozco ◽  
Francisco Hernández-Quiroz ◽  
Hector Zenil ◽  
Wilfried Sieg
Keyword(s):  
Propositional Calculus ◽  
Surprising Result ◽  
Free Lunch ◽  
Additional Information ◽  
Theorem Provers ◽  
Automatic Theorem Provers ◽  
No Free Lunch Theorem ◽  
Set Up ◽  
No Free Lunch ◽  
Automatic Theorem

There are many examples of failed strategies whose intention is to optimize a process but instead they produce worse results than no strategy at all. Many fall under the loose umbrella of the “no free lunch theorem”. In this paper we present an example in which a simple (but assumedly naive) strategy intended to shorten proof lengths in the propositional calculus produces results that are significantly worse than those achieved without any method to try to shorten proofs.This contrast with what was to be expected intuitively, namely no improvement in the length of the proofs. Another surprising result is how early the naive strategy failed. We set up a experiment in which we sample random classical propositional theorems and then feed them to two very popular automatic theorem provers (AProS and Prover9). We then compared the length of the proofs obtained under two methods: (1) the application of the theorem provers with no additional information; (2) the addition of new (redundant) axioms to the provers. The second method produced even longer proofs than the first one.

Implementing theorem provers in a purely functional style

1999 ◽  
Vol 9 (2) ◽  
pp. 147-166 ◽  
Author(s):  
KEITH HANNA
Keyword(s):  
Partial Algebra ◽  
Proof Assistant ◽  
Theorem Provers ◽  
Executable Specification ◽  
Efficient Representation

This paper discusses the principles of implementing an LCF-style proof assistant using a purely functional metalanguage. Two approaches are described; in both, signatures are treated as ordinary values, rather than as mutable components within an abstract datatype. The first approach treats the object logic as a partial algebra and represents it as a partial datatype, that is, a datatype in which the domains of the constructors are restricted by predicate functions. This results in a compact, executable specification of the logic. The second approach uses an abstract type to allow an efficient representation of the logic, whilst keeping the same interface. A case study describes how these principles were put into practice in implementing a fairly complex dependently-sorted logic.

Sign in / Sign up

Export Citation Format

Share Document