Course Description:In many applications, we expect computers to reason logically. We might naively expect this to be what computers are good at, but in fact they find it extremely difficult. In this overview course, we look briefly at several varieties of mechanical reasoning. The first is automated deduction, whereby conclusions are derived from assumptions purely by following an algorithm, without user intervention. Automated deduction procedures are parametrized by the logic they are capable of reasoning with. We distinguish between propositional logic and first-order logic. Development and application of propositional logic procedures, also called SAT solvers, received considerable attention in the last ten years, e.g., for solving constraint satisfaction problems, applications in hardware design, verification, and planning and scheduling. Regarding automated deduction in first-order logic, we discuss applications, standard deductive procedures such as resolution, and basic concepts, such as unification. We also examine the dual problem of theorem proving, viz., generating models of a given theory, which has applications to finding counterexamples for non-theorems. A third important area covered in the course is dealing with interactive theorem proving. Interactive theorem proving requires certain amount of instructions from the user to tell the proving program (the theorem prover) how to proceed with a proof. Such interaction is required usually because of the use of higher-order logics, whose expressive formalisms allow natural modeling of complex systems, such as operating system or various protocols. A recent trend in the development of interactive proving is to improve its automation, by combining the power of automatic provers.