Email Gateway (Aug 19 2022 at 08:52): Email Gateway (Aug 19 2022 at 08:52):From: Slawomir Kolodynski <skokodyn@yahoo.com>
it also works with Metamath somehow.
I translated about 600 proofs from Metamath to Isabelle/ZF. So it was the other way than what Michael asked about. There are some details in http://isarmathlib.org/MMI_prelude.html.
Slawomir Kolodynski
http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Email Gateway (Aug 19 2022 at 09:05):From: Michael Fridkin <michael.fridkin@gmail.com>
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
Email Gateway (Aug 19 2022 at 09:05):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 09:05):From: Makarius <makarius@sketis.net>
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
Last updated: May 06 2024 at 16:21 UTC