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

Isabelle has been developed over nearly 30 years, but with largely the same formalism; the only real changes have concerned polymorphism and type classes. Thanks to the LCF architecture, only a tiny percentage of the code has to be trusted. There are papers concerning formal properties of the basic calculus and some of its extensions, which should answer many specific questions. I would mention in particular the following papers:

L. C. Paulson. 
The foundation of a generic theorem prover. J. Automated Reasoning 5 (1989), 363–397.

Markus Wenzel 
Type classes and overloading in higher-order logic
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science Volume 1275, 1997, pp 307-322

Larry Paulson

On 4 Feb 2013, at 22:37, Steven Ericsson-Zenith <steven at> wrote:

> I'd say from the point of view of constructing real proofs this inaccessibility is a real problem. Are there proof statements concerning the formal properties of Isabelle?
> Steven

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