An Introduction to the Concepts and Techniques of Automated Theorem-Proving

This paper summarizes the theoretical foundations and basic methodology of automated theorem-proving. The material presented includes a review of the predicate calculus, the transformation of a first-order wff into clause normal form, J. A. Robinson's resolution principle, semantic resolution, significant resolution heuristics (search strategies), and paramodulation. The application of theorem-proving techniques to the problem of program correctness is also briefly discussed.