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.


	Makarius





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