Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Best of 2016 Recommended by Editor Recommended by Reviewer Recommended by Reader
Search
Formalization of the resolution calculus for first-order logic
Schlichtkrull A. Journal of Automated Reasoning61 (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?
yes
no
Other reviews under "Predicate Logic": Date
Probabilistic propositional logic
Guggenheimer H., Polytechnic University, Brooklyn, NY, 1987. Type: Book
Jan 1 1989
Modeling production rules by means of predicate transition networks
Giordana A., Saitta L. Information Sciences 35(1): 1-41, 1985. Type: Article
Oct 1 1985
Symbolic normalized acquisition and representation of knowledge
Bouchon B., Laurière J. Information Sciences 37(1-3): 85-94, 1985. Type: Article
Nov 1 1986
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy