Re: [isabelle] An ATP question
On 25 Oct 2012, at 20:22, Michael Fridkin <michael.fridkin at gmail.com> wrote:
Hi I would like to know if anyone has tried converting Isabelle/ZF or
even Isabelle/HOL proofs to Metamath format and then using an
evolutionary algorithm or any other search algorithm for automatic
proving, to be used with Sledgehammer?
On Fri, 26 Oct 2012, Lawrence Paulson wrote:
I don't know of any such work. In particular, as far as I know, nobody
has done much of anything with Isabelle/ZF apart from myself. It's a
pity, but set theory is a pretty obscure world.
It is not as bad. See this Isabelle/ZF based project in particular
http://isarmathlib.org/ -- it also works with Metamath somehow. You
should ask Slawomir (the project maintainer) himself for more details.
This archive was generated by a fusion of
Pipermail (Mailman edition) and