PhD course: Discrete structures and introduction to proofs
Description
The course is an introduction to the discrete math that computer scientists use. It piggybacks on the new undergraduate course "Discrete structures for computer science" given by Jörn Janneck, but goes into more depth and adds material on interactive proof assistants. If you already have taken a course similar to the undergraduate course (see EDAA40), you cannot get full points for this course.
Administrative details
- Course leader: Görel Hedin, gorel.hedin AT cs.lth.se
- Credits: 6 hp
- When: Spring 2016
- Sign up by emailing Görel.
Literature
Textbook: David Makinson: Sets, Logic and Maths for Computing, 2nd addition. It is freely available at the LU network here.
Additional material from EDAA40.
Material on the interactive proof assistant Coq:
Form
- Attend Jörn's lectures. Usually Mondays. Starting March 21, 10-12 in MA:3.
- Do the labs on your own.
- Read all chapters in the book, except for chapters 5 and 6 (combinatorics and probability).
- Do all the exercises in the corresponding chapters.
- Attend two video seminars on Coq.
- Do the related Coq exercises.
- Hand in solutions to End-of-Chapter exercises, and Coq exercises.
- Mark exercises from fellow students on one or more chapters.
Advice on exercises and labs
Concerning the exercises: It will be too much work to do and hand in all the End-of-Chapter exercises. Therefore, it is sufficient to hand in 1/4 of them, including the first subexercise of each. Example: In Chapter 1 there are four End-of-Chapter exercises: 1.1, 1.2, 1.3, and 1.4. Of these you should do:
- Exercise 1.1 (a), 1.2 (a), 1.3 (a), 1.4 (a)
- Since 1.1 has 8 subexercises (a-h), you select one additional, so that you do in total 8/4 = 2 subexercises of 1.1.
- For 1.2, which has 11 subexercises (1-k), you should do 11/4 = 3 (after rounding), so you select additionally two subexercises.
- Exercises 1.3 and 1.4 have only 3 subexercises each (a-c), so you don't have to do any extra here. The a) is sufficient.
- If you select any of the subexercises with subsubexercises, e.g., 1.1 f), which has 4 subsubexercises (i - iv), it is sufficient to select 4/4 = 1 again (i).
- Note that you should look at the other exercises too, to convince yourself that you could solve them. But you don't have to write them down and hand them in.
Advice for doing the exercises in Makinson's book. Try to follow the proofs. If you cannot prove something the way the book does it, try drawing a Venn diagram: Name all the different subsets in the diagram, and try to prove the statement that way. If you cannot do this, try to make an argument for why something is true.
Write your solutions for the Makinson exercises using pen and paper, not on the computer. Take a photo of your solution and email it to the marker, and with copy to Görel.
For the labs, email a zip file with your solution to the marker, and with copy to Görel.
For the Coq exercises: email your solved Coq file to the marker, and with copy to Görel.
All exercises and labs should be handed in by the deadline. All marking should be done within one week. Enter the results into the SAM system (PhD course in Discrete Structures).
If there are unclear things, exercises you could not solve, exercises with interesting solutions, let me (Görel) know, and we can gather the group and discuss.
Schedule
Week 12 (March 21...) Sets.
- Attend Jörn's lecture. Monday March 21, 10-12 in MA:3.
- Discussion fika. Wednesday March 23, 15:00-15:15, Coffeeroom.
- Read chapter 1 and do all exercises.
- Deadline for End-of-chapter solutions: Wednesday March 30.
- Exercise marker: Mattias Nordahl
Week 13 (March 28...) Relations.
- Attend Jörn's lecture. Tuesday March 29, 10-12 in MA:3.
- Discussion fika. Tuesday March 29, 15:00-15:15, Coffeeroom.
- Read chapter 2 and do all exercises.
- Deadline for End-of-chapter solutions: Monday April 4.
- Exercise marker: Alfred Åkesson
Week 14 (April 4...) Functions.
- Attend Jörn's lecture. Monday ...
- Discussion fika. Monday April 4, 15:00-15:15, Coffeeroom.
- Read chapter 3 and do all exercises.
- Deadline for End-of-chapter solutions: Monday April 11.
- Exercise marker: Mehmet Ali Arslan
Week 15 (April 11...) To infinity and beyond.
- Attend Jörn's lecture.
- Discussion fika. Monday April 11, 15:00-15:15, Coffeeroom.
Week 16 (April 18...) Induction and Recursion.
- Attend Jörn's lecture.
- Discussion fika. Monday April 18, 15:00-15:15, Coffeeroom.
- Do lab 1. Deadline: Monday April 25.
- Read chapter 4 and do all exercises.
- Deadline for End-of-chapter solutions: Monday April 25.
- Exercise marker: Niklas Fors
- Lab marker: Björn A Johnsson
Week 17 (April 25...) Trees and Graphs.
- Attend Jörn's lecture.
- Discussion fika. Monday April 25, 15:00-15:15, Coffeeroom.
- Do lab 2. Deadline: Monday May 2
- Read chapter 7 and do all exercises.
- Deadline for End-of-chapter solutions: Monday May 2.
- Exercise marker: Mårten Lager
- Lab marker: Mattias Nordahl
Week 18 (May 2...) Propositional logic.
- Attend Jörn's lecture.
- Discussion fika. Monday May 2, 15:00-15:15, Coffeeroom.
- Do lab 3. Deadline: Monday May 9
- Read chapter 8 and do all exercises.
- Deadline for End-of-chapter solutions: Monday May 9.
- Exercise marker: Alfred Åkesson
- Lab marker: Mehmet Ali Arslan
Week 20 (May 16...) Quantificational logic.
- Attend Jörn's lecture.
- Discussion fika. Monday May 16, 15:00-15:15, Coffeeroom.
- Do lab 4. Deadline: Monday May 23
- Read chapter 9 and do all exercises.
- Deadline for End-of-chapter solutions: Monday May 23.
- Exercise marker: Niklas Fors
- Lab marker: Björn A Johnsson
Week 21 (May 23...) Proofs.
- Attend Jörn's lecture.
- Discussion fika. Monday May 23, 15:00-15:15, Coffeeroom.
- Read chapter 10 and do all exercises.
- Deadline for End-of-chapter solutions: Tuesday May 30.
- Exercise marker: Mårten Lager
Week 22 (May 30...) Coq 1.
- Look through this video on installing CoqIDE.
- Look through this video introducing how to use CoqIDE.
- (More videos by the same guy are here, but you will probably not need them.)
- Download and install the latest version of CoqIDE from The Coq site.
- (Skip downloading the "proof general" Emacs plugin. I have not tried it, and you will not need it. CoqIDE is sufficient.)
- We will watch some of the lectures by Benjamin Pierce on Software foundations in Coq, from the Oregon Programming Languages Summer School 2012 summerschool (scroll down to the bottom of the page.)
- The videos are also available on YouTube on this playlist.
- Watch the two first videos: (37:15 + 15:44 minutes). This corresponds to the Preface and Basics in the book.
- Download the exercise set basics.v and solve it in CoqIDE.
- Deadline for handing in solutions: Tuesday June 7.
- Exercise marker: TBA
Week 23 (June 7...) Coq 2.
- Watch the two next videos (37:15 + 37:04 minutes). These cover Lists and Induction.
- Download the exercise set induction.v and solve it in CoqIDE.
- Deadline for handing in solutions: Thursday June 16.
- Exercise marker: TBA