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 term?"

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.