ENIGMA
| swMATH ID: | 28655 |
| Software Authors: | Jakubův, J.; Urban, J. |
| Description: | ENIGMA: Efficient Learning-Based Inference Guiding Machine. ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many previous proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, classifying a clause as useful or un-useful for the proof search. This learned classification is used to guide next proof searches prioritizing useful clauses among other generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E’s performance. |
| Homepage: | https://link.springer.com/chapter/10.1007%2F978-3-319-62075-6_20 |
| Related Software: | VAMPIRE; E Theorem Prover; MaLARea; Isabelle/HOL; DeepMath; MPTP 0.2; MaLeCoP; FEMaLeCoP; TacticToe; leanCoP; Mizar; HOList; XGBoost; BliStrTune; TPTP; HOL; LIBLINEAR; Coq; Flyspeck; Prover9 |
| Cited in: | 31 Documents |
Standard Articles
| 1 Publication describing the Software, including 1 Publication in zbMATH | Year |
|---|---|
|
Enhancing ENIGMA given clause guidance. Zbl 1417.68184 Jakubův, Jan; Urban, Josef |
2018
|
all
top 5
Cited by 43 Authors
Cited in 3 Serials
| 1 | Information Sciences |
| 1 | Journal of Automated Reasoning |
| 1 | AI Communications |
Cited in 4 Fields
| 31 | Computer science (68-XX) |
| 1 | Mathematical logic and foundations (03-XX) |
| 1 | Group theory and generalizations (20-XX) |
| 1 | Operations research, mathematical programming (90-XX) |
