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.
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.html

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
http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf

Larry Paulson


On 4 Feb 2013, at 22:37, Steven Ericsson-Zenith <steven at iase.us> 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.