Plan for SEM1A6 (Logic)

Mark Ryan

The module will be based on sections from the draft of a forthcoming book,

Logic in Computer Science: Modelling and Reasoning about Systems, by Michael Huth and Mark Ryan, to appear in 1999

which will be available as a handout. It will consist of two lectures per week and one exercise class. There are assessed exercises each week, which are to be handed in during the exercise class. One percentage point of the module is given for a serious attempt at the assessed exercises, so if you hand in all 10 you will get 10% of the marks before you take the exam.

The plan of the module is as follows:

Week 1 (25 Jan 1999).

The language of propositional logic. Parse trees. Introduction to natural deduction: the rules and-intro, and-elim, not-not, implies-elim, MT.

Sections from the book: 1.3 on parse trees; then 1.1, 1.2.1 (up to and including the section ``Rules for eliminating implication'').

Assessed exercises: p27 Q1(b,f), Q2, Q9; p5 Q4, Q5, Q10(a,e,h); p7 Q1 (to be handed in 1 Feb).

Week 2 (1 Feb).

More natural deduction: the rule implies-intro, the rules for or, the rules for not. Derived rules; RAA and LEM.

Sections from the book: 1.2.1 (rest), 1.2.2.

Assessed exercises: p10 Q2; p16 Q1(b), Q2(f,j,n,p,q) (to be handed in 8 Feb).

Week 3 (8 Feb).

Summary of natural deduction.

Sections from the book: 1.2.3, 1.2.4

Assessed exercises: p19 Q1 (a,b,f,g) Q2 (d); p24 Q1 (all of it) (to be handed in 15 Feb).

Week 4 (15 Feb).

Truth tables for propositional logic. Soundness and completeness (without proof). Introduction to binary decision diagrams.

Sections from the book: 1.4, 2.1 up to but excluding 2.1.3.

Assessed exercises: p31 Q2, Q3, Q5; p35 Q2; p38 Q1,2 (to be handed in 22 Feb).

Week 5 (22 Feb).

Binary decision diagrams.

Sections from the book: 2.1.3, 2.2.

Assessed exercises: p40 Q1(a), 3(b,d); p44 1(c); p48 8 (to be handed in 1 Mar).

Week 6 (1 Mar).

The language of Predicate logic.

Sections from the book: 3.1, 3.2.

Assessed exercises: p54 Q1(b,c), 2(b); p56 Q1, Q2, Q5 (to be handed in 8 Mar).

Week 7 (8 Mar).

This week is set aside for a recap and/or catching up. There will be lectures.

There are no exercises to be handed in on 15 March. Instead there will be a brief class test covering the material so far; if you get more than 40% then you get a bonus of 1 mark.

Week 8 (15 Mar).

Program logic. Correctness: partial and total. Hoare triples. A simple programming language. The rules for composition and assignment.

Sections from the book: 4.1, 4.2, 4.3.1, up to p67.

Assessed exercises: p73 Q1, Q2 (to be handed in 22 Mar).

Week 9 (22 Mar).

The rule for If-statements.

Sections from the book: up to p76.

Assessed exercises: p76 Q1, Q2 (to be handed in 26 Apr).

Week 10 (26 Apr).

The rule for while-loops.

Sections from the book: up to p79. sum section''.

Assessed exercises: p79 Q1, Q2, Q6 (to be handed in 3 May).

Week 11 (3 May).

Case study: Minimal-sum section.

Sections from the book: 4.3.3 (starts p79)

Assessed exercises: p81 Q1, Q3; p82 Q1 [looks rather complicated!] (to be handed in 10 May).

Week 12 (10 May).

Room for expansion; revision.