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.

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 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.

scholarly journals Improving ENIGMA-style Clause Selection while Learning From History

2021 ◽  
pp. 543-561
Author(s):  
Martin Suda
Keyword(s):  
Neural Network ◽  
Real Time ◽  
Theorem Prover ◽  
Central Idea ◽  
Theorem Provers ◽  
Recursive Neural Network ◽  
Time Evaluation ◽  
Automatic Theorem ◽  
Learning From History

AbstractWe re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recognizing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We propose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The automatic theorem prover Vampire guided by the network achieves a 41 % improvement on a relevant subset of SMT-LIB in a real time evaluation.

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 Aiming for the Goal with SInE

10.29007/q4pt ◽  
2020 ◽  
Author(s):  
Martin Suda
Keyword(s):  
Experimental Evaluation ◽  
Main Idea ◽  
Inference Engine ◽  
Theorem Prover ◽  
Selection Algorithm ◽  
First Order ◽  
Theorem Provers ◽  
The Individual ◽  
Goal Distance ◽  
Automatic Theorem

The Sumo INference Engine (SInE) is a well-established premise selection algorithm for first-order theorem provers, routinely used, especially on large theory problems. The main idea of SInE is to start from the goal formula and to iteratively add other formulas to those already added that are related by sharing signature symbols. This implicitly defines a certain heuristical distance of the individual formulas and symbols from the goal.In this paper, we show how this distance can be successfully used for other purposes than just premise selection. In particular, biasing clause selection to postpone introduction of input clauses further from the goal helps to solve more problems. Moreover, a precedence which respects such goal distance of symbols gives rise to a goal sensitive simplification ordering. We implemented both ideas in the automatic theorem prover Vampire and present their experimental evaluation on the TPTP benchmark.

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 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 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.

Sign in / Sign up

Export Citation Format

Share Document