v1v2 (latest)

BliStr: The Blind Strategymaker

12 January 2013

Papers citing "BliStr: The Blind Strategymaker"

26 / 26 papers shown

Title
Learning Conjecturing from Scratch Thibault Gauthier J. Urban LRM 80 1 0 03 Mar 2025
Solving Hard Mizar Problems with Instantiation and Strategy Invention Jan Jakubuv Mikoláš Janota Josef Urban 74 0 0 25 Jun 2024
Regularization in Spider-Style Strategy Discovery and Schedule Construction Filip Bártek Karel Chvalovský Martin Suda 65 7 0 19 Mar 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 93 5 0 06 Mar 2024
MizAR 60 for Mizar 50 Jan Jakubruv Karel Chvalovský Z. Goertzel C. Kaliszyk Mirek Olvsák Bartosz Piotrowski S. Schulz Martin Suda Josef Urban 87 13 0 12 Mar 2023
Alien Coding Thibault Gauthier Miroslav Olsák J. Urban 74 8 0 27 Jan 2023
The Isabelle ENIGMA Z. Goertzel Jan Jakubruv C. Kaliszyk Miroslav Olvsák Jelle Piepenbrock Josef Urban AIMat 49 13 0 04 May 2022
Learning Theorem Proving Components Karel Chvalovský Jan Jakubuv Miroslav Olsák Josef Urban LRM 51 8 0 21 Jul 2021
Fast and Slow Enigmas and Parental Guidance Z. Goertzel Karel Chvalovský Jan Jakubuv Miroslav Olsák Josef Urban 78 11 0 14 Jul 2021
Property Invariant Embedding for Automated Reasoning Miroslav Olsák C. Kaliszyk Josef Urban NAI 69 41 0 27 Nov 2019
ENIGMAWatch: ProofWatch Meets ENIGMA Z. Goertzel Jan Jakubuv Josef Urban 66 16 0 23 May 2019
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E Karel Chvalovský Jan Jakubuv Martin Suda Josef Urban 65 65 0 07 Mar 2019
Reinforcement Learning of Theorem Proving C. Kaliszyk Josef Urban Henryk Michalewski Miroslav Olsák 67 148 0 19 May 2018
Learning to Reason with HOL4 tactics Thibault Gauthier C. Kaliszyk Josef Urban 94 77 0 02 Apr 2018
ENIGMA: Efficient Learning-based Inference Guiding Machine Jan Jakubuv Josef Urban 76 94 0 23 Jan 2017
BliStrTune: Hierarchical Invention of Theorem Proving Strategies Jan Jakubuv Josef Urban 89 25 0 26 Nov 2016
Internal Guidance for Satallax Michael Färber C. Brown LRM 55 26 0 30 May 2016
Premise Selection and External Provers for HOL4 Thibault Gauthier C. Kaliszyk 62 47 0 11 Sep 2015
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems Sebastiaan J. C. Joosten C. Kaliszyk Josef Urban LRM 50 6 0 06 Jun 2014
Machine Learner for Automated Reasoning 0.4 and 0.5 C. Kaliszyk Josef Urban J. Vyskočil LRM 99 23 0 11 Feb 2014
Learning-assisted Theorem Proving with Millions of Lemmas C. Kaliszyk Josef Urban 119 47 0 11 Feb 2014
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 135 135 0 10 Oct 2013
Lemma Mining over HOL Light C. Kaliszyk Josef Urban 59 12 0 10 Oct 2013
HOL(y)Hammer: Online ATP Service for HOL Light C. Kaliszyk Josef Urban 112 95 0 19 Sep 2013
MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers D. Kühlwein Josef Urban 145 22 0 09 Aug 2013
Learning-Assisted Automated Reasoning with Flyspeck C. Kaliszyk Josef Urban LRM 141 163 0 29 Nov 2012