Email Gateway (Aug 22 2022 at 18:47): Email Gateway (Aug 22 2022 at 18:47):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
I found several people from the metamath community making experiments
with a neural Automated Theorem Prover for higher-order logic
named Holophrasm. I would like to know if there is some analogous
of Holophrasm for Isabelle/HOL in order to do some experiments too, but
using simple type theory in place of the metamath language (equivalent to
ZFC).
Some references concerning Holophrasm (for metamath):
Whalen, Daniel. "Holophrasm: a neural Automated Theorem Prover for
higher-order logic." arXiv preprint arXiv:1608.02644(2016).
https://arxiv.org/pdf/1608.02644.pdf
GitHub of Holophrasm: https://github.com/dwhalen/holophrasm
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 18:47):From: Josef Urban <josef.urban@gmail.com>
Dear Jose,
The closest and most finished work for the HOL logic in this line of
machine learning research is TacticToe by Thibault Gauthier et al. For
Isabelle, check the recent work (Pamper) of Yutaka Nagashima. For neural
attempts, Sarah Loos is working on a neural system similar to TacticToe for
HOL Light (probably unpublished yet, but maybe there are some slides from
the AITP conference - check there for more).
In the FOL ATP world there is a neural guided E prover by Sarah et al.,
ENIGMA by Jan Jakubuv et al., and rlCoP (reinforcement learning connection
prover) by Cezary Kaliszyk et al.
Best,
Josef
Last updated: Apr 26 2024 at 16:20 UTC