Schedule¶

CIS 301: Logical Foundations of Programming, Spring 2018

Lecture: T U 11:05am - 12:20pm, DUE1073

Links:

Slides
Examples:

Week. Day: Date	Lecture	Remarks
T: Jan 16	Course Administration [video] 301 Tool Setup slides [video is included in Course Administration video] Introduction: Why Bother? [study guide]	Reading: Introduction: Why Bother? Tool setup: (see Tools)
U: Jan 18	Circuits and Truth Tables [examples, FYTD solutions, study guide]	Reading: Circuits and Truth Tables HW 1 Assigned (see the Assignments section of 301 Canvas) HW 1 direct link) Extended deadline Monday, January 29 at 11:59pm
T: Jan 23	Circuits and Truth Tables [examples, FYTD solutions, study guide]	Reading: Circuits and Truth Tables Reading (from Logic in Action): Chapter 2. Propositional Logic Optional: Chapter 3. Syllogistic Reasoning
U: Jan 24	Introduction to Propositional Logic [FYTD #1a solution, FYTD #1b solution, example, study guide]	Reading (from Logic in Action): Chapter 2. Propositional Logic Optional: Chapter 3. Syllogistic Reasoning
T: Jan 30	English Language to Propositional Logic [FYTD #1 solution, study guide]	Reading: Translating Between English and Propositional Logic (Scott Martin, Ohio State); Logic and Critical Reasoning (Chapter 6 only)
U: Feb 1	Automatic Reasoning for Propositional Logic [example, FYTD #1 solution, FYTD #2 solution, FYTD #3 solution (building truth tables), FYTD #4 solution (checking tautologies), FYTD #5 solution (sequents, validity, equivalences), Exercises, Guided Exercise: Basic SAT (.txt, video), Guided Exercise: Finding more models and building truth tables (.txt, video)]	Reading: Z3’s Guide (up to Section 3 on Propositional Logic)
T: Feb 6	(Catch up day)
U: Feb 8	Introduction to Natural Deduction [study guide] Natural Deduction – And [examples, FYTD #1 solution]	Reading: Applications of Propositional Logic to Program Proving (up to Section 7.3)
T: Feb 13	Natural Deduction – Or [examples, FYTD #1 solution, FYTD #2 solution, FYTD #3 solution]	Reading: Applications of Propositional Logic to Program Proving (Section 7.4) Instructor Travel (Department of Homeland Security research meeting)
U: Feb 15	Natural Deduction – Implies [examples, FYTD #1 solution, FYTD #2 solution]	Reading: Applications of Propositional Logic to Program Proving (Section 7.5)
T: Feb 20	Natural Deduction – Negation [Lecture video: Bottom Elimination Rule, Lecture video: Proof-by-Contradiction Rule, examples, FYTD #1-1, FYTD #1-2, FYTD #2, FYTD #3-1, FYTD #3-2, FYTD #4, FYTD #5]	Reading: Applications of Propositional Logic to Program Proving (Section 7.6 - 7.7)
U: Feb 22	Natural Deduction – Negation [Lecture video: Bottom Elimination Rule, Lecture video: Proof-by-Contradiction Rule, examples, FYTD #1-1, FYTD #1-2, FYTD #2, FYTD #3-1, FYTD #3-2, FYTD #4, FYTD #5]	Reading: Applications of Propositional Logic to Program Proving (Section 7.6 - 7.7)
T: Feb 27	Curry-Howard Isomorphism [Lecture video, examples]	Optional Background Reading: Classical vs. Constructive Logic Exercises HW 4 Assigned (see the Assignments section of 301 Canvas) HW 4 direct link, Deadline Friday, March 9 at 11:59pm
U: Mar 1	Quantifications by Example (no slides for this lecture, only code examples) [Lecture video, Scala examples, Java examples] Introduction to Predicate Logic [Lecture video: (part a), (part b), (part c coming later), examples, Z3 examples, FYTD #1-1, FYTD #1-2, FYTD #2-1, FYTD #2-2]
T: Mar 6	Introduction to Predicate Logic [examples, Z3 examples, FYTD #1-1, FYTD #1-2, FYTD #2-1, FYTD #2-2]	Reading: The Predicate-Logic Quantifiers (up to Section 8.2)
U: Mar 8	Algebra [Z3 examples] Programming Logic for Assignment [examples]	Reading: Circuits that Compute on Numbers: Algebra
T: Mar 13	Exam 1 [references, study guides]	Reading: (none)
U: Mar 15	Programming Logic for Assignment [examples, FYTD #1 (starting file, solution), FYTD #2 (starting file, solution)]	Reading: Programming Logic for Assignments and Conditionals (up to Section 4.1)
Spring Break
T: Mar 27	Programming Logic for Assignment [Lecture video: (part b), examples, FYTD #1 (starting file, solution), FYTD #2 (starting file, solution)]	Reading: Programming Logic for Assignments and Conditionals (Section 4.2) HW 5 Assigned (see the Assignments section of 301 Canvas) HW 5 direct link, Deadline Wednesday, April 4, 11:59pm
U: Mar 29	Programming Logic for Assignment [Lecture video: (part b), examples, FYTD #1 (starting file, solution), FYTD #2 (starting file, solution)]	Reading: Programming Logic for Assignments and Conditionals (Section 4.2)
T: Apr 3	Programming Logic for Conditionals and Loops [Lecture video: (conditionals - part a), conditional #1, conditional #2] [loop invariants recipe, auto, symexe]	Reading: Loop, Invariants, Induction
U: Apr 5	Programming Logic for Conditionals and Loops [loop invariants recipe, auto, symexe]
T: Apr 10	Sequences [#1, #2, #3 (manual), #3 (auto), #3 (symexe), #4]
U: Apr 12	Sequences [#1, #2, #3 (manual), #3 (auto), #3 (symexe), #4]
T: Apr 17	Functions and Procedures [examples]	Reading: Functions and Procedures
U: Apr 19	Functions and Procedures [examples, java]	Reading: Functions and Procedures
T: Apr 24	Exam 2 [references]
U: Apr 26	Recursion [examples: #1, #2, #3, #4]
T: May 1	Termination [examples, Collatz: Logika, Java]
U: May 3	Closing Remarks Review for Final Exam
Monday: May 7	Final Exam, Time: 9:40am - 11:30am [references, study guides]