*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 04 Feb 2013 22:44:36 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1302041610580.9980@macbroy21.informatik.tu-muenchen.de>*References*: <1359754874943@names.co.uk> <510D7F55.5000902@gmx.com> <alpine.LNX.2.00.1302041610580.9980@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 2/4/2013 9:16 AM, Makarius wrote:

On Sat, 2 Feb 2013, Gottfried Barrow wrote:I now ask, "Where is the semi-formal definition of a Isabelle typeand term?"If you said, "If you understand the HOL4 definitions of a type andterm, then you basically understand Isabelle's".See the Isabelle/Isar implementation manual chapter 2, aboutIsabelle/Pure as reduced version of Higher-Order Logic to provide thelogical framework.

Makarius,

In truth the greatest challenge is from having to deal with performances unfolding in front of you that are just so astounding and abnormal that you know precisely what's happening but you just can't say it straight out. The list is endless; Rasmussen, Armstrong and the Postals, Sella, Ricco, Mazzoleni... and on. I now confine myself to saying "that was an unbelievable performance"...

http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/isar-ref.pdf

http://www4.in.tum.de/~berghofe/papers/TPHOLs2000.pdf

http://arxiv.org/ftp/cs/papers/9301/9301105.pdf

http://www.amazon.com/Isabelle-Generic-Theorem-Lecture-Computer/dp/3540582444 And on page 5 they're already talking about type classes. (Makarius writes)

This is occasionally interesting to know, although just some tinyfoundational bit. From Isabelle/Pure you move on to Isabelle/HOL,then you add many add-on tools for 'inductive', 'datatype' etc. andlots of proof tools like Sledgehammer. Then you are quite high abovethe logical foundations and don't care much about them.

Regards, GB

What is also interesting that the final end-user view tends toconverge to what totally different systems offer here, e.g. Coq withits quite different foundations, if you take inductive definitions orrecursive functions, for example.Makarius

**Follow-Ups**:**Re: [isabelle] Where to learn about HOL vs FOL?***From:*Makarius

**References**:**Re: [isabelle] Where to learn about HOL vs FOL?***From:*"Mark"

**Re: [isabelle] Where to learn about HOL vs FOL?***From:*Gottfried Barrow

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

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] afp_build in RC2
- Previous by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list