Re: [isabelle] Where to learn about HOL vs FOL?
On Wed, Feb 6, 2013 at 2:49 PM, Makarius <makarius at sketis.net> wrote:
> 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
> 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".
I was not at all expecting it to be like the other implementations of HOL.
I am aware of the Isabelle framework. However, I was expecting to find
something resembling higher-order logic, that is, the logic Isabelle/HOL
purports to implement. The way that is put together using the framework is
still somewhat obscure to me, and there is no one reference to learn about
it. However there are plenty I should read more of.
> 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