HOL(y)Hammer: Online ATP Service for HOL Light

19 September 2013

Papers citing "HOL(y)Hammer: Online ATP Service for HOL Light"

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
Proof Automation with Large Language Models Minghai Lu Benjamin Delaware Tianyi Zhang LRM 84 9 0 22 Sep 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
JEFL: Joint Embedding of Formal Proof Libraries Qingxiang Wang C. Kaliszyk 51 0 0 21 Jul 2021
Vampire With a Brain Is a Good ITP Hammer Martin Suda 71 12 0 06 Feb 2021
Superposition with Lambdas Alexander Bentkamp J. Blanchette Sophie Tourret Petar Vukmirović Uwe Waldmann 38 34 0 31 Jan 2021
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction Yutaka Nagashima LRM 69 3 0 19 Oct 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
Mathematical Reasoning in Latent Space Dennis Lee Christian Szegedy M. Rabe Sarah M. Loos Kshitij Bansal 83 34 0 26 Sep 2019
Computer-aided proofs for multiparty computation with active security Helene Haagh Aleksandr Karbyshev Sabine Oechsner Bas Spitters Pierre-Yves Strub 51 27 0 19 Jun 2018
Universal Reasoning, Rational Argumentation and Human-Machine Interaction Christoph Benzmüller LRM AI4CE 18 9 0 28 Mar 2017
Premise Selection and External Provers for HOL4 Thibault Gauthier C. Kaliszyk 67 47 0 11 Sep 2015
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
Machine Learning of Coq Proof Guidance: First Experiments C. Kaliszyk L. Mamane Josef Urban LRM 51 17 0 20 Oct 2014
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems Sebastiaan J. C. Joosten C. Kaliszyk Josef Urban LRM 55 6 0 06 Jun 2014
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description C. Kaliszyk Josef Urban J. Vyskočil H. Geuvers 74 24 0 14 May 2014
Machine Learner for Automated Reasoning 0.4 and 0.5 C. Kaliszyk Josef Urban J. Vyskočil LRM 109 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