A step-by-step presentation of the code for a small theorem prover introduces theorem-proving techniques. The programming language used is Standard ML. The prover operates on a sequent calculus formulation of first-order logic, which is briefly explained. The implementation of unification and logical inference is shown. The prover is demonstrated on several small examples, including one that shows its limitations. The final part of the paper is a survey of contemporary research on interactive theorem proving.
arXiv comments
Journal reference
published in S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (editors), Handbook of Logic in Computer Science, Vol II (Oxford, 1992), 415-475
Linked by 2 identifiable commenters in 2 comments across 2 threads, from May 2024 to Feb 2025. Found in 1 HN submission from Feb 2025 to Feb 2025. Open submission discussions.
Hi nill0, please don’t link directly to pdfs on arxiv, but the abstract page instead. Like this: https://arxiv.org/abs/cs/9301110 The reader can decide if they want to go further. Thanks. Also, enjoying your submissions, but please pace yourself.
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
Hi nill0, please don’t link directly to pdfs on arxiv, but the abstract page instead. Like this: https://arxiv.org/abs/cs/9301110 The reader can decide if they want to go further. Thanks. Also, enjoying your submissions, but please pace yourself.
yo_yo_yo-yoView on HNParent context