Macock, Deborah Y.2013-06-192013-06-191975http://hdl.handle.net/10919/20271This 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.application/pdfenIn CopyrightTechnical reportCS75024-Rhttp://eprints.cs.vt.edu/archive/00000803/01/CS75024-R.pdf