Re: [isabelle] Where to learn about HOL vs FOL?
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 Isabelle/HOL, then
you add many add-on tools for 'inductive', 'datatype' etc. and lots of
proof tools like Sledgehammer. Then you are quite high above the logical
foundations and don't care much about them.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and