# CS 3234 - Logic and Formal Systems, Semester 1 2010-2011

## Brief Description

The module aims to cover both classical and non-classical logics focusing on their deductive and algorithmic aspects. It introduces mathematical logic as a means for specifying, verifying and reasoning about computer programs. Its emphasis, in contrast to other similar logic modules, is on how logic can be used to represent computational problems, how these representations can be proved correct and how they can be executed on a computer. Topics covered include classical logic theories, modal logic, program specfication and verification and typing.

## Material

The module material (slides, notes) is accessible in the following table.

Lecture Date Subject Slides Notes
01 12/8 Introduction Slides 01 in color
Slides 01 in B/W
-
02 19/8 Traditional Logic Slides 02 in color
Slides 02 in B/W
Coq script used in lecture
Coq cheat sheet (v1)
03 26/8 Induction and Propositional Logic Slides 03a in color (Induction)
Slides 03a in B/W (Induction)
Slides 03b in color (Propositional Logic)
Slides 03b in B/W (Propositional Logic)
Notes on Induction
Coq script (induction) used in lecture
Notes on Propositional Logic
Coq script (propositional logic) used in lecture
04 2/9 Propositional Logic II; Predicate Logic I Slides 04a in color (Propositional Logic II)
Slides 04a in B/W (Propositional Logic II)
Slides 04b in color (Predicate Logic I)
Slides 04b in B/W (Predicate Logic I)
Notes Propositional Logic II
Notes Predicate Logic I
05 9/9 Predicate Logic II Slides 05a in color (Predicate Logic II)
Slides 05a in B/W (Predicate Logic II)
Slides 05b (Insights into Coq proofs)
Notes Predicate Logic II
Coq script on variable scoping
Cheat sheet (explicit propositions vs builtin propositions)
Cheat sheet on predicate logic
06 15/9 Induction; midterm midterm test (including solutions)
Coq script for midterm (Questions 8, 9 and 10)
(For practicing, take a look at last year's midterm test, including solutions)
Slides 06 on induction (but the notes on induction given as suplementary reading in the next week are better)
Notes on formal induction
Coq script on induction
07 30/9 An application of SAT solving
An application of theorem proving
Induction in Coq
Slides 07a in color (Propositional Logic: Application of SAT Solving)
Slides 07a in B/W (Propositional Logic: Application of SAT Solving)
Slides 07b in color (Application of predicate logic and increasing trustworthiness)
-
08 7/10 Modal Logic I Slides 08 in color Slides 08 in B/W Notes on Modal Logic I
09 14/10 Modal Logic II Slides 09 in color Slides 09 in B/W Notes on Modal Logic I (including Coq)
Coq script on Modal Logic I
10 21/10 Program verification I Slides 10 in Color (Program verification I) Notes on Hoare Logic (covering I and II, updated)
11 28/10 Program verification II Slides 11a in Color (Program verification II) Slides 11b in Color (Semantics of Hoare Logic) Notes on Hoare Logic (covering I and II, updated)
12 4/11 The lambda calculus Slides 12

The lectures use the tool Coq extensively. You can download this tool from the Coq homepage. Here is a local copy for faster loading:

## Assignments

Assignments are distributed online in this section. Submission as indicated in the assignments. The solutions are discussed in the tutorial session after submission, see calendar above.

 Assignment Date handed out Time due Assignment Solution Assignment 1 18/8 26/8, 11:00am Assignment 1 Solution Assignment 2 26/8 2/9, 11:00am Assignment 2 Solution Assignment 3 2/9 9/9, 11:00am Assignment 3 Solution Assignment 4 1/10 7/10, 11:00am Assignment 4 Solution Assignment 5 9/10 14/10, 10:30am Assignment 5 Solution Assignment 6 19/10 25/10, 5:00pm Assignment 6 Solution Assignment 7 29/10 5/11, 5:00pm Assignment 7 Solution

## Labs, Coq Homework and Quizzes

Coq homework and quizzes are distributed online in this section. The solutions are discussed in the lab session after submission, see calendar above.

 Homework/Quiz Date handed out Time due Solution Homework 1 18/8 27/8, 9:30pm Homework 1 Solution For free play, use Wedding_Cakes.v, and Wedding_Cakes_solution.v. Quiz 01, to practice, here are three more Lewis Carroll puzzles Propositional_Logic_Lab.v: Script for propositional logic (partially covered during the lab) 1/9 1/9 Quiz 01 Solution Homework 2 Propositional_Logic_Lab2.v: Script for propositional logic 3/9 10/9, 9:30pm Homework 2 Solution Quiz 02 Quiz 02 A, Quiz 02 B 10/9 10/9 Quiz 02 Solution A, Quiz 02 Solution B Quiz 03 Quiz 03 A, Quiz 03 B to practice, here are a few Coq exercises Slower example Slower example in text-based format 29/9 29/9 Quiz 03 Solution A, Quiz 03 Solution B Coq homework 3 30/9 8/10 Solution to Coq induction homework Quiz 04 Quiz 04 Group A, Quiz 04 Group B 13/10 and 20/10 13/10 and 20/10 Quiz 04 Solution A by Hanrui/Sally Quiz 04 Solution B by Hanrui/Sally Coq homework 4 15/9 22/10 Coq homework 4 solution by Hanrui/Sally Quiz 05 Quiz 05 Group A, Quiz 05 Group B 27/10 27/10 Quiz 05 Solution A by Hanrui/Sally Quiz 05 Solution B by Hanrui/Sally Coq homework 5 31/10 7/11 Coq homework 5 solution Coq Workshop (Lab Week 12) 3/11 - - Quiz 06 Quiz 06 Group A, Quiz 06 Group B 10/11 10/11 Quiz 06 Solution A Quiz 06 Solution B Quiz 06 Solution A by Hanrui/Sally Quiz 06 Solution B by Hanrui/Sally

## More Module Information

Assessment
Final: 54%
for practice see 2008 final (note that different topics were covered)
2009 final and
2009 final Coq part
Format:
• Open book (any written and printed material is allowed; no electronic aides)
• Time: overall two hours any part of which can be spent freely on paper and Coq parts
• Paper part: around 60% of marks for final, answer all questions
• Coq part: around 40% of marks for final, answer 4 out of 5 questions
Midterm: 10%
Assignments: 7 times 2% = 14%
Coq Homework: 5 times 2% = 10%
Coq Quizzes: 6 times 2% = 12%
Attendance of labs: Lab attendance is mandatory. You are allowed to miss one of the 11 labs. Any missed lab beyond one leads to a deduction of 1% of the overall assessment (in addition to possibly missing a quiz). Coming late for more than 10 minutes is considered missing the lab. You are allowed to leave early, in those lab sessions that end in a quiz.
Mounting Information
Elective module for students in the Bachelor of Computing programmes of the School of Computing
Modular credits: 4
Prerequisites: Pass CS 1102