Use of computers for forming deductions and proving theorems in symbolic logic covered. Topics include resolution, unification, proof strategies, and equality. Also examines areas of application: problem solving, question answering, program verification, automatic programming and logic programming (Prolog).