*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Question Posed: Where is a good place to learn about HOL?*From*: gottfried.barrow at gmx.com*Date*: Fri, 01 Jun 2012 14:15:39 -0500*In-reply-to*: <201205310412.q4V4CCrj014777@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205251146380.8953@macbroy22.informatik.tu-muenchen.de> <201205270818.q4R8IUWm022240@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205292251410.19391@macbroy22.informatik.tu-muenchen.de> <201205310412.q4V4CCrj014777@poisson.math.northwestern.edu>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

From: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle On 5/30/2012 11:12 PM, Bill Richter wrote:

...Let me make a rudimentary FOL point: I think writing down strict axiomatic FOL proofs would really be tedious because e.g. you have manually substitute variables every time you want to use an axiom.

Listing the books below is the purpose of this reply.

Also, as you may have observed on hol info, I know next to nothing about HOL... Where is a good place to learn about HOL?

1) Natural deduction logic 2) Lambda calculus

4) The ML programming language 5) The meta-logic of Isabelle/Pure

-----NATURAL DEDUCTION LOGIC---

"Proof and Disproof in Formal Logic", by Richard Bornat (Amazon) This books is what I'm working through. Some of it's written like

the Jape prover for doing some natural deduction exercises. http://www.cs.ox.ac.uk/people/bernard.sufrin/personal/jape.org/ "Mathematical Logic", by Ian Chiswell & Wilfrid Hodges (Amazon)

referred to in the Isabelle literature. "Logic for Computer Science", by Jean H. Gallier (Amazon) More advanced. I use it to try and find unfamiliar terminology. "Natural Deduction", by Dag Prawitz (Amazon)

"Logic for Computer Science", by Steve Reeves and Mike Clarke (Amazon)

http://en.wikipedia.org/wiki/Method_of_analytic_tableaux ---LAMBDA CALCULUS & TYPED LAMBDA CALCULUS---

serve their purpose to drive the points in. "Type Theory & Functional Programming", by Simon Thompson (Amazon)

types as proofs, and proofs as types. "Basic Simple Type Theory", by J. Roger Hindley (Amazon)

combinatory logic. "Foundations of Functional Programming", by Lawrence Paulson A quick summary of lambda calculus. http://www.cl.cam.ac.uk/~lp15/papers/Notes/Founds-FP.pdf

"Lambda Calculi with Types", by Henk Barendregt (Amazon) "Types and Programming Language", by Benjamin C. Pierce (Amazon) "Lecture Notes on Lambda Calculus", by Peter Selinger http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf ---ML PROGRAMING LANGUAGE---

"ML for the Working Programmer", 2nd, by Larry Paulson (Amazon) "Programming in Standard ML '97", by Stephen Gilmore http://homepages.inf.ed.ac.uk/stg/NOTES/ "Introduction to Functional Programming", by Mike Gordon http://www.cl.cam.ac.uk/~mjcg/Teaching/FuncProg/Notes/ "Programming in Standard ML", by Robert Harper http://www.cs.cmu.edu/~rwh/smlbook/ "Notes on Programming Standard ML of New Jersey", by Riccardo Pucella http://www.ccs.neu.edu/home/riccardo/research.html "Elements of ML Programming", by Jeffrey D. Ullman (Amazon) ---META-LOGIC OF ISABELLE/PURE---

Paulson: http://www.cl.cam.ac.uk/~lp15/papers/refereed.html Isabelle - The Next 700 Theorem Provers The Foundation of a Generic Theorem Prover Urban: http://www.inf.kcl.ac.uk/staff/urbanc/Cookbook/ The Isabelle Cookbook Wenzel: http://www4.in.tum.de/~wenzelm/papers/

From the Isabelle2012 release: Old Introduction to Isabelle The Isabelle/Isar Reference Manual A Proof Assistant for Higher-Order Logic ---BEST BOOK I'VE FOUND SO FAR---

--GB

**Follow-Ups**:**Re: [isabelle] Question Posed: Where is a good place to learn about HOL?***From:*gottfried . barrow

- Previous by Date: Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features
- Next by Date: Re: [isabelle] Question Posed: Where is a good place to learn about HOL?
- Previous by Thread: Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features
- Next by Thread: Re: [isabelle] Question Posed: Where is a good place to learn about HOL?
- Cl-isabelle-users June 2012 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