Aims

• To introduce the notation and main concepts of logic, and to appreciate some of its uses in computer science.
• To introduce some concepts in program specification and verification.

• Understand the syntax, proof theory and semantics of propositional logic, and to perform natural deduction proofs. Understand some methods of representing and computing with propositional logic formulas.
• Understand the syntax of predicate logic, and to have an informal appreciation of what formulas mean and how they are used. To be able to code up sentences involving quantifiers and predicates.
• Use logic to describe programs and data, and to reason about them by producing proofs.
• Understand how program logics can be used to reason about simple imperative programs, and how an appreciation of pre- and post- conditions can help write correct programs.
• Produce proofs in program logic about the correctness of simple programs involving assignments, conditionals, and the while loop.

• None.

Two lectures and one exercise class per week, throughout the semester.

Notes on this course are provided, with extensive examples and exercises. The lectures emphasise the key points, explain in detail concepts and algorithms, and go through detailed examples.

Assessment

10% continuous: there are assessed exercises each week, which are to be handed in during the exercise class. One percentage point of the module is given each week for a serious attempt at the
assessed exercises.

90% written examination.

Recommended Books

Title	Author(s)	Publisher	Comments
Lecture Notes for SEM1A6	Mark Ryan	unpublished	Essential
Reasoned programming	K. Broda, S. Eisenbach, H. Khoshnevisan, S. Vickers	Prentice Hall, 1994.	Further reading
Program construction and verification	Roland C. Backhouse	Prentice-Hall 1986	Further reading

• Propositional logic. The language of propositioinal logic.  Natural deduction. The rules of natural deduction.  Derived rules.  Theorem provers. Parse trees. Truth tables; Soundness and completeness (without proof). [4 weeks]
• Binary decision diagrams. Representing propositional formulas. Algorithms `reduce' and `apply'. [1 week]

• Predicate  logic. The language of Predicate logic. Predicates, functions, variables, quantifiers. [2 weeks]
• Program logic.  Partial and total correctness.  Hoare triples.  A simple programming language. The rules for composition and  assignment. The rule for If-statements.  Invariants and the rule for while-loops.  Case study: Minimal-sum section.[4 weeks]

Week by week plan for 1999.