This module focuses on the deductive and algorithmic aspects of both classical and non-classical logics. It introduces logic as a means for specifying, verifying and reasoning about computer programs. It emphasises, in contrast to other similar logic courses, on how logic can be used to represent computational problems, how these representations can be proven correct and how they can be executed on a computer. Topics covered include classical logic theories, logic programming, modal logic, and an introduction to non-standard logics. Treatments of predicate calculus and temporal logic are fully covered with emphasis on their specification, verification, deductive and algorithmic aspects.