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.

The use of neural network and discrete Fourier transform for real-time evaluation of friction stir welding

2011 ◽  
Vol 11 (8) ◽  
pp. 4839-4846 ◽  
Author(s):  
Enkhsaikhan Boldsaikhan ◽  
Edward M. Corwin ◽  
Antonette M. Logar ◽  
William J. Arbegast
Keyword(s):  
Neural Network ◽  
Fourier Transform ◽  
Friction Stir Welding ◽  
Real Time ◽  
Discrete Fourier Transform ◽  
Friction Stir ◽  
Time Evaluation

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.

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

Sign in / Sign up

Export Citation Format

Share Document