Re: [isabelle] Where to learn about HOL vs FOL?



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.
I would anticipate it to be much easier for HOL Zero, and know it to be
fairly easy for HOL4 and HOL Light.
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.


On Mon, Feb 4, 2013 at 7:21 PM, Yannick Duchêne (Hibou57) <
yannick_duchene at yahoo.fr> wrote:

> Le Mon, 04 Feb 2013 16:16:43 +0100, Makarius <makarius at sketis.net> a
> écrit:
>
>
>  On Sat, 2 Feb 2013, Gottfried Barrow wrote:
>>
>>  I now ask, "Where is the semi-formal definition of a Isabelle type and
>>> term?"
>>>
>>> If you said, "If you understand the HOL4 definitions of a type and term,
>>> then you basically understand Isabelle's".
>>>
>>
>> See the Isabelle/Isar implementation manual chapter 2, about
>> Isabelle/Pure as reduced version of Higher-Order Logic to provide the
>> logical framework. This is occasionally interesting to know, although just
>> some tiny foundational bit.  From Isabelle/Pure you move on to Isabelle/HOL,
>>
>
> But Isabelle/HOL is entirely derived from Isabelle/Pure, isn't it?
>
>
>  What is also interesting that the final end-user view tends to converge
>> to what totally different systems offer here, e.g. Coq with its quite
>> different foundations, if you take inductive definitions or recursive
>> functions, for example.
>>
>
> People seems to care, only when they have to port some proof from one
> system to another. There seems to be multiple HOL4 to Isabelle papers on
> the web, and seems all are concerned with foundations.
>
>
> --
> “Syntactic sugar causes cancer of the semi-colons.” [1]
> “Structured Programming supports the law of the excluded muddle.” [1]
> [1]: Epigrams on Programming — Alan J. — P. Yale University
>
>
>




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