🔗 Who cites «HOL(y)Hammer: Online ATP Service for HOL Light»

9 papers of our library cite it (of the 149,439 whose bibliographies we read) · 7 with a page here, the most cited first · ← back to «HOL(y)Hammer: Online ATP Service for HOL Light»

1. MizAR 40 for Mizar 40Journal of Automated ReasoningCezary Kaliszyk, Josef Urban2013 · 112 citations
2. History of Interactive Theorem ProvingHandbook of the History of Logic, vol. 9 (Elsevier)John Harrison, Josef Urban, Freek Wiedijk2014 · 109 citations
3. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem ProversarXiv:2205.10893Albert Q. Jiang, Wenda Li, Szymon Tworkowski, et al.2022 · 79 citations
4. ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)Lecture notes in computer scienceJan Jakubův, Karel Chvalovský, Miroslav Olšák, et al.2020 · 42 citations
5. Magnushammer: A Transformer-Based Approach to Premise SelectionarXiv:2303.04488Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, et al.2023 · 35 citations
6. Property Invariant Embedding for Automated ReasoningFrontiers in artificial intelligence and applicationsMiroslav Olšák, Cezary Kaliszyk, Josef Urban2019 · 30 citations
7. Premise Selection for a Lean HammerarXiv:2506.07477Thomas Zhu, Joshua Clune, Jeremy Avigad, et al.2025 · 5 citations

2 more papers of our library cite it; they have no page here yet.

This page in Markdown → https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/cited-by/