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

On Wed, 6 Feb 2013, Ramana Kumar wrote:

I was not at all expecting it to be like the other implementations of HOL. I am aware of the Isabelle framework. However, I was expecting to find something resembling higher-order logic, that is, the logic Isabelle/HOL purports to implement.

That is in principle src/HOL/HOL.thy, which is based on the original Cambridge HOL report by Mike Gordon. Note that some of the axiomatic bits have been moved to other Isabelle theories over the years, such as Hilbert choice to src/HOL/Hilbert_Choice.thy.

The way that is put together using the framework is still somewhat obscure to me, and there is no one reference to learn about it.

But this is where things really happen, and what makes the difference. Rules are specified as "axioms" in user-space, and the system composes them according to the principles introduced by Larry Paulson 25 years ago.


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