Resolution Theorem Proving
M.E. Stickel · Annual Review of Computer Science · 1988
The resolution theorem-proving method was developed by J. A. Robinson in about 1 963 (Robinson 1 965a) and is still one of the most important methods of automated deduction. Many good books present various parts of the material that we can only present briefly and informally here. Chang & Lee (1973) was the first textbook for resolution, paramodulation, and unification, and is still useful. Loveland ( 1978) and Bibe1 ( 1982) are more recent texts excep tionally strong in the areas of linear refinements of resolution and the connection method, respectively. Wos et al (1984) is written for a wider audience and reflects the practical experience with resolution theorem proving at Argonne National Laboratory; it is especially strong in the areas of deciding how to formalize problems and how to select strategies for their solution. A recent companion book (Wos 1988) presents a list of 33 basic research problems in resolution theorem proving. Siekmann & Wrightson (1983) contains many important early papers in resolution theorem proving. Kowalski ( 1979b) emphasizes the important connections between resolution theorem proving and logic programming. Manna & Waldinger (1985) and Gallier ( 1986) are new textbooks in symbolic logic, oriented toward computer sicence and automated deduction. McDermott's ( 1987) review article discusses resolution theorem proving in less detail but places it in the context of logic, problem solving, and deduction in general. A review like this must occasionally omit entire topics as well as details. The most important topic that we are unable to discuss is unification. Siekmann (1987) should be consulted for a comprehensive survey of results on unification algorithms that could be used in resolution theorem proving.