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

Calendar

For lecture, tutorial, lab, office hour, quiz, exam times, and assignment and homework submission deadlines, see the calendar below.

News

Notes on Traditional Logic, second set of slides, first assignment and first Coq homework are available below.

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
 Notes on Traditional Logic
Coq script used in lecture
Coq cheat sheet (v1)
Cheat sheet for traditional logic
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) 		-
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)
Coq script on induction 		Notes on formal induction
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 10/9 10/9 Quiz 02 Solution A,
Quiz 02 Solution B
Quiz 03
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:
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
Workload
2-1-2-2-2
Explanation: A-B-C-D-E
A: no. of lecture hours per week
B: no. of tutorial hours per week
C: no. of lab hours per week
D: no. of hours for projects, assignments, fieldwork etc per week
E: no. of hours for preparatory work by a student per week
Instructors

Martin Henz and Aquinas Hobor