HNGlance

Top Best New Show

The Foundation of a Generic Theorem Prover (1989) [pdf]

https://arxiv.org/pdf/cs/9301105

by 082349872349872 • 2 years ago

59 4 2 years ago

AR

Related Stories

Loading related stories...

Comments

4

i_don_t_know• 2 years ago

See also “Designing a Theorem Prover” 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

zermelo44• 2 years ago

Great 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• 2 years ago

Any suggestions for those papers?

hackandthink• 2 years ago

What are the limits of a generic implementation?

The individual object calculi are already complicated, when does the meta-logic reach its limits?

Source preview

arxiv.org

HNGlance

© 2024-2026 HN Glance. Story content belongs to its original sources.

Privacy
Terms