Premise Selection and External Provers for HOL4

11 September 2015

Papers citing "Premise Selection and External Provers for HOL4"

22 / 22 papers shown

Title
Premise Selection for a Lean Hammer Thomas Zhu Joshua Clune Jeremy Avigad Albert Qiaochu Jiang Sean Welleck 24 0 0 09 Jun 2025
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction Liao Zhang David M. Cerna C. Kaliszyk 59 0 0 02 Nov 2024
Magnushammer: A Transformer-Based Approach to Premise Selection Maciej Mikuła Szymon Tworkowski Szymon Antoniak Bartosz Piotrowski Albert Qiaochu Jiang Jinyi Zhou Christian Szegedy Lukasz Kuciñski Piotr Milo's Yuhuai Wu 161 46 0 08 Mar 2023
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers Albert Q. Jiang Wenda Li Szymon Tworkowski K. Czechowski Tomasz Odrzygó'zd'z Piotr Milo's Yuhuai Wu M. Jamnik AIMat LRM 94 103 0 22 May 2022
A Classification of Artificial Intelligence Systems for Mathematics Education S. Van Vaerenbergh Adrián Pérez-Suay 31 13 0 13 Jul 2021
Online Machine Learning Techniques for Coq: A Comparison Liao Zhang Lasse Blaauwbroek Bartosz Piotrowski Prokop Cerný C. Kaliszyk Josef Urban OffRL 44 11 0 12 Apr 2021
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning Minchao Wu Michael Norrish Christian J. Walder Amir Dezfouli 71 42 0 19 Feb 2021
Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text Deborah Ferreira André Freitas AIMat 60 32 0 30 Apr 2020
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) Jan Jakubuv Karel Chvalovský Miroslav Olsák Bartosz Piotrowski Martin Suda Josef Urban 65 44 0 13 Feb 2020
Property Invariant Embedding for Automated Reasoning Miroslav Olsák C. Kaliszyk Josef Urban NAI 69 41 0 27 Nov 2019
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic Thibault Gauthier 56 13 0 25 Oct 2019
Towards Finding Longer Proofs Zsolt Zombori Adrián Csiszárik Henryk Michalewski C. Kaliszyk Josef Urban OffRL LRM 93 16 0 30 May 2019
ENIGMAWatch: ProofWatch Meets ENIGMA Z. Goertzel Jan Jakubuv Josef Urban 66 16 0 23 May 2019
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving Kshitij Bansal Sarah M. Loos M. Rabe Christian Szegedy S. Wilcox AIMat 101 51 0 05 Apr 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
TacticToe: Learning to Prove with Tactics Thibault Gauthier C. Kaliszyk Josef Urban Ramana Kumar Michael Norrish 88 55 0 02 Apr 2018
Learning to Reason with HOL4 tactics Thibault Gauthier C. Kaliszyk Josef Urban 94 77 0 02 Apr 2018
BliStrTune: Hierarchical Invention of Theorem Proving Strategies Jan Jakubuv Josef Urban 89 25 0 26 Nov 2016
Monte Carlo Tableau Proof Search Michael Färber C. Kaliszyk Josef Urban 79 14 0 18 Nov 2016
Sharing HOL4 and HOL Light proof knowledge Thibault Gauthier C. Kaliszyk 44 23 0 11 Sep 2015
Certified Connection Tableaux Proofs for HOL Light and TPTP C. Kaliszyk Josef Urban J. Vyskočil 77 23 0 20 Oct 2014