MaLARea
MaLARea: a Metasystem for Automated Reasoning in Large Theories. MaLARea (a Machine Learner for Automated Reasoning) is a simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS ATP systems) with a machine learning component (now the SNoW system used in the naive Bayesian learning mode). Its intended use is in large theories, i.e. on a large number of problems which in a consistent fashion use many axioms, lemmas, theorems, definitions and symbols. The system works in cycles of theorem proving followed by machine learning from successful proofs, using the learned information to prune the set of available axioms for the next theorem proving cycle. Although the metasystem is quite simple (ca. 1000 lines of Perl code), its design already now poses quite interesting questions about the nature of thinking, in particular, about how (and if and when) to combine learning from previous experience to attack difficult unsolved problems. The first version of MaLARea has been tested on the more difficult (chainy) division of the MPTP Challenge solving 142 problems out of 252, in comparison to E’s 89 and SPASS ’ 81 solved problems. It also outperforms the SRASS metasystem, which also uses E and SPASS as components, and solves 126 problems.
Keywords for this software
References in zbMATH (referenced in 44 articles )
Showing results 1 to 20 of 44.
Sorted by year (- Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
- England, Matthew; Florescu, Dorian: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition (2019)
- Rawson, Michael; Reger, Giles: A neurally-guided, parallel theorem prover (2019)
- England, Matthew: Machine learning for mathematical software (2018)
- Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
- Piotrowski, Bartosz; Urban, Josef: ATPboost: learning premise selection in binary setting with ATP feedback (2018)
- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef: TacticToe: learning to reason with HOL4 tactics (2017)
- Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
- Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam: Detecting inconsistencies in large first-order knowledge bases (2017)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
- Jan Jakubuv, Josef Urban: BliStrTune: Hierarchical Invention of Theorem Proving Strategies (2016) arXiv
- Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef: Mizar: state-of-the-art and beyond (2015)
- Furbach, Ulrich; Pelzer, Björn; Schon, Claudia: Automated reasoning in the wild (2015)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
- Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří: Lemmatization for stronger reasoning in large theories (2015)
- Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)