References

  1. David Auger, Adrien Couëtoux & Olivier Teytaud (2013): Continuous Upper Confidence Trees with Polynomial Exploration - Consistency. In: Machine Learning and Knowledge Discovery in Databases - European Conference, ECML PKDD 2013, Prague, Czech Republic, September 23-27, 2013, Proceedings, Part I, pp. 194–209, doi:10.1007/978-3-642-40988-2_13.
  2. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy & Stewart Wilcox (2019): HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In: Kamalika Chaudhuri & Ruslan Salakhutdinov: Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, Proceedings of Machine Learning Research 97. PMLR, pp. 454–463. Available at http://proceedings.mlr.press/v97/bansal19a.html.
  3. Yves Bertot (2008): A Short Presentation of Coq. In: Otmane Ait Mohamed, César Muñoz & Sofiène Tahar: Conference on Theorem Proving in Higher Order Logics (TPHOLs), LNCS 5170. Springer, pp. 12–16, doi:10.1007/978-3-540-71067-7_3.
  4. Lasse Blaauwbroek, Josef Urban & Herman Geuvers (2020): The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. In: Christoph Benzmüller & Bruce R. Miller: Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, LNCS 12236. Springer, pp. 271–277, doi:10.1007/978-3-030-53518-6_17.
  5. Karel Chvalovský, Jan Jakubuv, Martin Suda & Josef Urban (2019): ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. In: Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, pp. 197–215, doi:10.1007/978-3-030-29436-6_12.
  6. Thibault Gauthier (2020): Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. In: Elvira Albert & Laura Kovács: LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, EPiC Series in Computing 73. EasyChair, pp. 230–248, doi:10.29007/7jmg.
  7. Thibault Gauthier (2020): Tree Neural Networks in HOL4. In: Christoph Benzmüller & Bruce R. Miller: Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, LNCS 12236. Springer, pp. 278–283, doi:10.1007/978-3-030-53518-6_18.
  8. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar & Michael Norrish (2021): TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65(2), pp. 257–286, doi:10.1007/s10817-020-09580-x.
  9. John Harrison (2009): HOL Light: An Overview. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Conference on Theorem Proving in Higher Order Logics (TPHOLs), LNCS 5674. Springer, pp. 60–66, doi:10.1007/978-3-642-03359-9_4.
  10. Joe Hurd (2005): System Description: The Metis Proof Tactic. In: Carsten Schuermann Christoph Benzmueller, John Harrison: Workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), pp. 103–104. Available at https://arxiv.org/pdf/cs/0601042.
  11. Cezary Kaliszyk, Josef Urban, Henryk Michalewski & Miroslav Olsák (2018): Reinforcement Learning of Theorem Proving. In: Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi & Roman Garnett: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pp. 8836–8847. Available at https://proceedings.neurips.cc/paper/2018/hash/55acf8539596d25624059980986aaa78-Abstract.html.
  12. Yutaka Nagashima & Yilun He (2018): PaMpeR: proof method recommendation system for Isabelle/HOL. In: Marianne Huchard, Christian Kästner & Gordon Fraser: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018. ACM, pp. 362–372, doi:10.1145/3238147.3238210.
  13. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, Yutian Chen, Timothy Lillicrap, Fan Hui, Laurent Sifre, George van den Driessche, Thore Graepel & Demis Hassabis (2017): Mastering the game of Go without human knowledge. Nature 550, pp. 354–359, doi:10.1038/nature24270.
  14. Konrad Slind & Michael Norrish (2008): A Brief Overview of HOL4. In: Otmane Aït Mohamed, César A. Muñoz & Sofiène Tahar: Conference on Theorem Proving in Higher Order Logics (TPHOLs), LNCS 5170. Springer, pp. 28–32, doi:10.1007/978-3-540-71067-7_6.
  15. Makarius Wenzel, Lawrence C. Paulson & Tobias Nipkow (2008): The Isabelle Framework. In: Otmane Aït Mohamed, César A. Muñoz & Sofiène Tahar: Conference on Theorem Proving in Higher Order Logics (TPHOLs), LNCS 5170. Springer, pp. 33–38, doi:10.1007/978-3-540-71067-7_7.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org