Re: [isabelle] An ATP question

On 25 Oct 2012, at 20:22, Michael Fridkin <michael.fridkin at> 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 -- 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 MHonArc.