Re: [isabelle] An ATP question



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.

Larry Paulson


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?
> 
> --Michael






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