Re: [isabelle] A neural Automated Theorem Prover for higher-order logic



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


On Sun, Nov 25, 2018, 12:53 José Manuel Rodriguez Caballero <
josephcmac at gmail.com wrote:

> 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.
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.