Are you interested in proof assistants in which human experts guide automatic theorem provers to verify subgoals? The paper focuses on research dedicated to a theoretical aim: applying a special proof assistant to produce human-readable rigorous proofs for fundamental theorems of mathematical logic, especially for those that provide the bases of theorem provers themselves. This investigation has advantages for both fields.
First, the author introduces the notions of first-order logic and discusses proof methods of Herbrand’s theorem, fundamental to automatic theorem provers. Then the chosen formalization is described and explained. Examples show how the Isar language can express the notions and inferences for writing structured derivations and proofs of statements that humans can read.
The primary, novel achievement of the research is to find a way to prove the soundness and completeness of the resolution calculus by applying a proof assistant. The rich apparatus of the Isabelle/HOL system is explored. It is a sophisticated proof assistant implementation of higher-order logic (HOL).
The paper emphasizes the most challenging parts of the formalization: the substitution lemma, Herbrand’s theorem, and the lifting lemma. The notions and notation, syntax and semantics, and theory and meta-theory must be carefully and clearly defined. The application of a dedicated proof assistant helps in thoroughly investigating and cleaning existing proofs. Moreover, it strengthens well-known statements. Therefore, the approach improves the quality of the theory.
The author gives a detailed overview of related work. Results from inference systems utilizing the completeness of first-order logic are characterized.
The paper’s layered structure, clear phrasing, exposition of motivations, discussions, and examples are helpful to readers. Recommended reading for those interested in mathematical logic and the development of human-readable precise proofs with proof assistants.