BliStr
BliStr: The Blind Strategymaker. BliStr is a system that automatically develops strategies for E prover on a large set of problems. The main idea is to interleave (i) iterated low-timelimit local search for new strategies on small sets of similar easy problems with (ii) higher-timelimit evaluation of the new strategies on all problems. The accumulated results of the global higher-timelimit runs are used to define and evolve the notion of ”similar easy problems”, and to control the selection of the next strategy to be improved. The technique was used to significantly strengthen the set of E strategies used by the MaLARea, PS-E, E-MaLeS, and E systems in the CASC@Turing 2012 competition, particularly in the Mizar division. Similar improvement was obtained on the problems created from the Flyspeck corpus.
Keywords for this software
References in zbMATH (referenced in 16 articles )
Showing results 1 to 16 of 16.
Sorted by year (- Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
- Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
- Jakubův, Jan; Urban, Josef: Hierarchical invention of theorem proving strategies (2018)
- 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)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Jakubův, Jan; Urban, Josef: Extending E prover with similarity based clause selection strategies (2016)
- 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)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (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)
- Kühlwein, Daniel; Urban, Josef: MaLeS: a framework for automatic tuning of automated theorem provers (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
- Kaliszyk, Cezary; Urban, Josef: Lemma mining over HOL Light (2013)