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 easy thing.

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 time there.

Someone interested in Open Theory output should look there again.


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