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