*To*: Mark <mark at proof-technologies.com>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Sat, 02 Feb 2013 15:04:21 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1359754874943@names.co.uk>*References*: <1359754874943@names.co.uk>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 2/1/2013 3:41 PM, "Mark" wrote:

Does that clear anything up?

Mark,

Regards, GB

I think it can get quite confusing because different people use the same names for different things, and different names for the same things, and sometimes the same people do this too! "HOL" can mean "higher-order logic" (referring to one or more of various logics that are higher-order), or it can mean "the HOL logic" (Mike Gordon's particular higher-order logic, implemented by HOL4, Isabelle/HOL, HOL Light, ProofPower and HOL Zero). Other theorem provers such as Coq, PVS and IMPS implement other higher-order logics. So the logic described in the HOL4 logic manual really is the same as HOL Light's, etc, the only difference being that they are built up in different ways (i.e. they start with a different initial set of axioms and primitive inference rules, but these axiomatisations are just different ways of defining the same logic). Does that clear anything up? Mark. on 1/2/13 2:23 PM, Gottfried Barrow<gottfried.barrow at gmx.com> wrote:On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:Seems available on‑line; here is a link for the paper you suggest: http://www.sciencedirect.com/science/article/pii/S157086830700081X# (the page also has a link at the top, for a PDF version)There's a newer dated version, 20 December 2007, at the author's web site. The published one says "received in revised form 6 August 2007". http://imps.mcmaster.ca/doc/seven-virtues.pdf http://imps.mcmaster.ca/doc/ When the gurus try to succinctly describe Isabelle/HOL, they'll many times just use the phrase "simply typed lambda calculus". https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus But if they have time to type a few extra characters, they might add the phrase "with polymorphism". If you keep talking long enough, another one might pop in and throw in the term "type classes". Because there's no HOL which has yet won the HOL wars, then they use external, historical vocabulary to begin the description of their HOL, but then have to start attaching their own internal vocabulary to the description. For someone looking for a label to label HOL with, as a starting place to learn about HOL, it can get confusing. If you see the phrase "simple type theory" in the title of Farmer's paper, then you might ask, "Ah, is this what's going to tell me what Isabelle/HOL is? Because 'simple type theory' sounds suspiciously like 'simply typed lambda calculus'". https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types Being an authoritative prophet, I can now say that in the future, the HOL's which win out in the HOL wars will be the standard themselves, and the references will be to the 700 page textbooks which formalize, starting with the basics, what the logic of these HOLs are. For HOL4 they already have that in their logic manual (to what degree I can't say), which I thought would be the perfect place to learn about Isabelle/HOL's formal logic, but it's not, it's the perfect place to learn about HOL4's formal logic: http://hol.sourceforge.net/documentation.html For completeness, I quote from Mark's glossary to show how the gurus have to do a lot qualifying when they try to explain things: simply-typed : (adj) Relating to type systems that are relatively simple and are not, for example, dependently-typed. There is considerable variationinthe precise intended meaning of "simply-typed" in contemporary usage: in some usages polymorphism is not a disqualifying factor, in other usages polymorphismisonly a disqualifying factor if it caters for the quantification of type variables, and in other usages still any form of polymorphism is a disqualifying factor. To avoid confusion, the usage of this term is avoided in HOL Zero, its documentation and elsewhere in this glossary.Still looking at Gottfried's list.In addition to collecting books, I also rip web pages for past, educational courses on Isabelle. I haven't had time to study any of this right now. I'm making enough progress just stumbling along. I'll get more sophisticated later. Some of these are linked to from the official Isabelle site, many of them aren't. Regards, GB http://www.phil.cmu.edu/~avigad/formal/ http://www.andrew.cmu.edu/user/avigad/isabelle/ http://www4.in.tum.de/~ballarin/belgrade08-tut/ http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php http://isabelle.in.tum.de/coursematerial/IJCAR04/ http://archiv.infsec.ethz.ch/education/permanent/csmr.html http://isabelle.in.tum.de/exercises/ http://www.irisa.fr/celtique/genet/ACF/ http://dream.inf.ed.ac.uk/projects/isabelle/ http://isabelle.in.tum.de/coursematerial/PSV2009-1/ http://www21.in.tum.de/teaching/logik/SS12/ http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/ http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/ http://www.cs.colorado.edu/~siek/7000/spring07/ http://ecee.colorado.edu/~siek/ecen3703/spring10/ECEN_3703.html http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php http://www.lri.fr/~wenzel/Isar2010-Orsay/ http://www.lri.fr/~wenzel/Isabelle2011-Paris/ http://www.lri.fr/~wenzel/Isabelle_Orsay_2012/ http://www.lri.fr/~wenzel/Isabelle_Orleans_2012/

**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"

- Previous by Date: Re: [isabelle] Trying to fix pretty printing for "syntax" & "translations"
- Next by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- 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