Description: Review of prepositional and first-order logic. Herbrand’s theorem. The resolution principle. Semantic resolution and lock resolution. Linear resolution. The equality relation. Some proof procedures based on Herbrand’s theorem. Program analysis. Deductive question answering, problem solving and program synthesis. Implementation of a theorem prover.