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

Le Fri, 01 Feb 2013 15:22:53 +0100, Gottfried Barrow <gottfried.barrow at> a écrit:


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:

The one titled “Logic” (file name “kananaskis-8-logic.pdf”) still says in the preface:

This material was written by Andrew Pitts in 1991, and was
originally part of DESCRIPTION. Because this logic is shared
with other theorem-proving systems (HOL Light, ProofPower),
and is similar to that implemented in Isabelle, where it is
called Isabelle/HOL, it is now presented in its own manual.

“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.