4 ms·
The Foundation of a Generic Theorem Prover (1989) [pdf]
- i_don_t_know 2y agoSee also “Designing a Theorem Prover” https://arxiv.org/pdf/cs/9301110 https://arxiv.org/pdf/cs/9301110 And chapter 10 of ML for the working programmer, freely available at https://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html https://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html
- 082349872349872 2y ago[flagged]
- deleted 2y ago[deleted]
- zermelo44 2y agoGreat paper for exploring the foundations of Isabelle. It's a shame the rest of the literature needed to properly understand Isabelle is scattered amongst many papers.
- timmg 2y agoAny suggestions for those papers?
- hackandthink 2y agoWhat are the limits of a generic implementation? The individual object calculi are already complicated, when does the meta-logic reach its limits?