Designing a Theorem Prover

TL;DR

This paper presents the design and implementation of a small theorem prover in Standard ML, demonstrating techniques like unification and inference, and surveys current research in interactive theorem proving.

Contribution

It provides a detailed step-by-step implementation of a theorem prover based on sequent calculus, including unification and inference, with practical examples and a research survey.

Findings

Prover operates on sequent calculus for first-order logic

Implementation of unification and logical inference techniques

Demonstrates limitations through small examples

Abstract

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.