Fun Stuff
-
Logicomix (web-page) by A. Doxiadis and C. Papadimitriou, Bloomsbury Publishing, 2009. A graphic novel subtitled `An Epic Search for Truth’ starring Russel, Whitehead, Frege, Goedel, Turing and many
-
Every computer scientist should also know xkcd, which releases new comics (on Romance, sarcasm, math, and language) every week.
Study Material
Archive of old Exams, Exercises, and More:#
Note that the course has been heavily revised, so the content will only loosely overlap with content from previous years. In particular, there are many topics which will not be covered this year, such as automata and Turing Machines.
Check out our Sharepoint that contains past exams, exercises, tutorial sheets, videos, and more! Definitely worth a look. To access the files, you will have to click on “Documents”. Within the folder displayed you find all our material.
Keep in mind that this is just intended as additional study material. Copying is strictly forbidden as this would be academic misconduct.
Short Videos Going through Examples:#
Those videos are a few years old, in particular (way) older than 2024.
- 01 Boolean Logic
- 02 Propositional Natural Deduction
- 03 First Order Natural Deduction
- 04 Induction
- 05 Hoare Logic and 06 Intro to Hoare Logic
- 07 Hoare Logic with Loops + Total Correctness
You may also visit the course’s old YouTube channel to check out other useful videos! The credit for all these videos and the YouTube channel goes to David Quarel, one of our previous tutors. (Kudos!)
Reading Material
By Topic / Lecture Week#
Note that the topics provided here are still according to the years up to 2023. This year, the course has been significantly revised. That said, there is still some overlap so that a lot of the material will still be helpful. However, the new material on Dafny is not covered below.
| Topic | Reference |
|---|---|
| Propositional Logic | [1] Chs 1.1, 1.2, 1.3, and 1.5 [2] Ch 3 [3] Ch 2 [4] Chs 1.1 and 1.2 [5] Chs 2.1, 2.2, 2.3, 2.4, 2.5, and 3.2 |
| Logic as Algebra | [1] Chs 1.4, 1.6, 2.1, and 2.4 [2] Ch 3 [3] Ch 2 [4] Chs 1.1 and 1.2 [5] Chs 2.1, 2.2, 2.3, 2.4, 2.5, and 3.2 |
| First Order Logic | [1] Chs 2.2, 2.3, 2.4, 2.5, 3.1, 3.2, and 3.3 [2] Ch 4 [3] Ch 3 [4] Chs 1.3 and 1.4 [5] Ch 2.6 [7] Chs 12 and 13 |
| All About Induction | [1] Ch 3.1 [2] Ch 5.1 [3] Chs 5.2, 5.3 and 5.6 [4] Ch 3.5 [5] Chs 3.4 and 3.5 |
| Induction for DataTypes | [1] Chs 3.3 |
| Hoare Logic (partial) | [1] Chs 9.4.1, 9.4.2, 9.4.3, and 9.5 [6] Chs Hoare Logic, Part I and Hoare Logic, Part II [7] [8] [9] |
| Hoare Logic (total) | [1] Chs 9.4.1, 9.4.2, 9.4.3, and 9.5 [6] Chs Hoare Logic, Part I and Hoare Logic, Part II [7] [8] [9] |
[1]: Winfried Karl Grassmann and Jean-Paul Tremblay. 1996. Logic and Discrete Mathematics: A Computer Science Perspective. Prentice Hall Press, Upper Saddle River, NJ, USA.
[2]: Willem Conradie, Valentin Goranko and Claudette Robinson. 2015. Logic and Discrete Mathematics: a concise Introduction. Chichester, West Sussex, United Kingdom : Wiley. (Available online via the ANU library.)
[3]: Susanna S. Epp. 2010. Discrete Mathematics with Applications. Brooks/Cole Publishing Co., Pacific Grove, CA, USA. (Available online via the ANU library.)
[4]: David J. Hunter. 2010. Essentials of Discrete Mathematics (2nd ed.). Jones and Bartlett Publishers, Inc., USA. (Available online via the ANU library.)
[5]: Harris Kwong. 2015. A Spiral Workbook for Discrete Mathematics. Amazon Digital Services LLC. (Available online here.)
[6]: Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. 2018. Programming Language Foundations. Software Foundations series, volume 2. Electronic textbook. (Available here (volume 2).)
[7]: Gordon, “Specification and Verification I”, online.
[8]: C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (October 1969), 576-580. doi: 10.1145/363235.363259. (Available here.)
[9]: Floyd, R. W. 1967. Assigning Meanings to Programs. Proceedings of Symposium on Applied Mathematics, 19, 19-32. (Available here.)
Further Reading Material#
The following are recommended references for the first six weeks excluding Dafny, for which we have a separate section (below).
-
Discrete Mathematics with Applications (3e) Susanna Epp, (Thomson-Brooks/Cole).
-
The Logic Book Merrie Bergmann, (McGraw-Hill).
-
Discrete Mathematics for Computing John Munro, (Thomas Nelson).
-
Mathematical Logic by Chiswell and Hodges, Oxford University Press, 2007. A very thorough and readable introduction to the topic.
-
Reasoned Programming by Krysia Broda, Susan Eisenbach, Hessam Khoshnevisan and Steven Vickers, Prentice Hall 1994. The first part is a bit dated by now, but the second part is a very usable introduction to first-order logic. Available electronically via the URL above.
-
forall x by P. D. Magnus. Another gentle introduction to first order logic, available electronically via the link above.
-
Some students have suggested this website. While it is not an official resource for the course, you might find it useful.
Further Reading Material on Dafny#
- Video Resources:
- on tree induction
- on loop invariants
- A short collection of videos by Rustan Leino on specification and verification in Dafny
- A written getting started with Dafny tutorial
- Textbook: Program Proofs by K. Rustan M. Leino
Further Reading Material on Haskell#
-
On Haskell tips, one of our previous tutors (from 2022), Pramo Samarasinghe, has created a short introduction to Haskell. It also contains the Haskell code used in lecture slides and tutorial sheets (update: this probably refers to the code that was previously in the first part and has now been replaced) with the corresponding explanation. Also, as written on our page for the the Lectures page, Haskell is not essential for this course anymore.
-
Haskell: The Craft of Functional Programming (2e) Simon Thompson, (Addison Wesley). (Many of you will have this book from COMP1100.)
-
On Haskell tips, our previous tutor (year not recorded) Benjamin Gray has created this. You might find it useful.