Re: [isabelle] Where to learn about HOL vs FOL?
On Tue, 5 Feb 2013, Ramana Kumar wrote:
As someone who once attempted to write an exporter from Isabelle/HOL to
OpenTheory, I have to say that figuring out exactly what the primitive
inference rules for Isabelle/HOL are and how they are used is not an
It is important to understand Isabelle/HOL as an application of the
Isabelle framework (a very large and important one), not as a variant of
"HOL", like HOL4, HOL-Light, HOL-XYZ. I am not surprised that it was
difficult to see the logical content there in the belly of Isabelle, if
you are expecting it to be just like "HOL".
My attempt in Isabelle is on hold at the moment; the last thought was to
see if I could use the existing proof-recording technology (Berghofer et
al) and translate the proof terms it creates into OpenTheory proofs.
There have been some references and links in this thread that I haven't
examined in detail yet, though, so thanks.
The proof terms by Stefan Berghofer are indeed the main starting point.
This aspect of Isabelle has been refined several times over the years, the
last time in Spring 2010 when we tried hard to make everything exportable
in principle, but the practical proof of it was still missing. Since then
there was a lack of significant applications, to justify spending too much
Someone interested in Open Theory output should look there again.
This archive was generated by a fusion of
Pipermail (Mailman edition) and