José Manuel Rodriguez Caballero
2018-11-25 11:52:05 UTC
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.
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.