Re: [isabelle] Where to learn about HOL vs FOL?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Where to learn about HOL vs FOL?
- From: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>
- Date: Thu, 26 Dec 2013 12:35:38 +0100
- Organization: Ada @ Home
- References: <op.wrrj47uzule2fv@cardamome> <510A79F0.firstname.lastname@example.org> <CAAPnxw2g6Di9MEmQgyqhf_+NBW5HLrVAPi2JVxohcFLTqWe1dA@mail.gmail.com>
- User-agent: Opera Mail/12.16 (Linux)
I'm adding this one:
“What does one need, when she needs higher‑order logic”?
It's about cases where a translation from second/higher order to first
order is possible; which may be seen as a way to get a strict
identification of what's unique to orders above the first.
Unfortunately, it's not easy to read (at least to me), as it refers to
example predicates which seems to be defined elsewhere.
Le Thu, 31 Jan 2013 16:51:59 +0100, Alfio Martini
<alfio.martini at acm.org> a écrit:
Adding to Gottfried´s selected readings, I strongly recommend the highly
"The Seven Virtues of Simple Type Theory' by William Farmer (Journal of
Applied Logic 6, 2008.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and