Re: [isabelle] Where to learn about HOL vs FOL?
Le Mon, 04 Feb 2013 16:16:43 +0100, Makarius
<makarius at sketis.net> a écrit:
On Sat, 2 Feb 2013, Gottfried Barrow wrote:
I now ask, "Where is the semi-formal definition of a Isabelle type and
If you said, "If you understand the HOL4 definitions of a type and
term, then you basically understand Isabelle's".
See the Isabelle/Isar implementation manual chapter 2, about
Isabelle/Pure as reduced version of Higher-Order Logic to provide the
logical framework. This is occasionally interesting to know, although
just some tiny foundational bit. From Isabelle/Pure you move on to
But Isabelle/HOL is entirely derived from Isabelle/Pure, isn't it?
What is also interesting that the final end-user view tends to converge
to what totally different systems offer here, e.g. Coq with its quite
different foundations, if you take inductive definitions or recursive
functions, for example.
People seems to care, only when they have to port some proof from one
system to another. There seems to be multiple HOL4 to Isabelle papers on
the web, and seems all are concerned with foundations.
“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