Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Formalization of the resolution calculus for first-order logic
Schlichtkrull A.  Journal of Automated Reasoning 61 (1-4): 455-484, 2018. Type: Article
Date Reviewed: Oct 26 2018

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.

Reviewer:  K. Balogh Review #: CR146297 (1901-0005)
Bookmark and Share
  Editor Recommended
Predicate Logic (I.2.4 ... )
Would you recommend this review?
Other reviews under "Predicate Logic": Date
Probabilistic propositional logic
Guggenheimer H.,  Polytechnic University, Brooklyn, NY, 1987.Type: Book
Jan 1 1989
A first-order conditional logic for prototypical properties
Delgrande J.  Artificial Intelligence 33(1): 105-130, 1987. Type: Article
Sep 1 1988
Test-score semantics as a basis for a computational approach to the representation of meaning
Zadeh L. (ed)  Literary & Linguistic Computing 1(1): 24-35, 1986. Type: Article
Aug 1 1987

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2019 ThinkLoud, Inc.
Terms of Use
| Privacy Policy