Schedule¶

CIS 301: Logical Foundations of Programming, Fall 2017

Lecture: T U 9:30am - 10:45am, 1073 Durland Hall

Links:

Slides
Study Guides
Examples: Truth Table, Z3, Propositional Logic, Predicate Logic, Programming Logic
Exercises
For You To Dos (FYTDs)
Tools: Logika, IntelliJ (Git Integration), Z3, Git

Week. Day: Date	Lecture	Remarks
T: Aug 22	Course Administration Introduction: Why Bother? [study guide]	Reading: Introduction: Why Bother? Tools: Install Sireum/Logika (see quick start videos)
U: Aug 24	Circuits and Truth Tables [examples, study guide]	Reading: Circuits and Truth Tables
T: Aug 29	Introduction to Propositional Logic [fytd #2, study guide]	Reading (from Logic in Action): Chapter 2. Propositional Logic Optional: Chapter 3. Syllogistic Reasoning Homework 1, Deadline: September 7, 2017, 11:59pm US Central
U: Aug 31	English Language to Propositional Logic [exercise]	Reading: Translating Between English and Propositional Logic (Scott Martin, Ohio State), Logic and Critical Reasoning (Chapter 6 only)
T: Sep 5	Automatic Reasoning of Propositional Logic [examples, Z3 Tutorial & Online]	Reading: Z3’s Guide (up to Section 3 on Propositional Logic)
U: Sep 7	Introduction to Natural Deduction Natural Deduction – And [examples]	Reading: Applications of Propositional Logic to Program Proving (up to Section 7.3) Homework 2, Deadline: September 18, 2017, 11:59pm US Central
T: Sep 12	Natural Deduction – Or [examples, fytd #1]	Reading: Applications of Propositional Logic to Program Proving (Section 7.4)
U: Sep 14	Natural Deduction – Implies [examples] Natural Deduction – Negation [examples]	Reading: Applications of Propositional Logic to Program Proving (Section 7.5)
T: Sep 19	Natural Deduction – Negation [examples]	Reading: Applications of Propositional Logic to Program Proving (Section 7.6 - 7.7) Homework 3, Deadline: September 27, 2017, 11:59pm US Central
U: Sep 21	Curry-Howard Isomorphism [examples: java, scala]	Optional Background Reading: Classical vs. Constructive Logic
T: Sep 26	No Lecture	Instructor Office Hours: 9:30-11:30am
U: Sep 28	Review for Exam 1 [exercises: solutions]
T: Oct 3	Exam 1 [references, study guides]
U: Oct 5	Quantifications & Predicates by Example [scala, java] Predicate Logic [examples, Z3 examples]	Reading: The Predicate-Logic Quantifiers (up to Section 8.2)
T: Oct 10	Predicate Logic [examples, Z3 examples]	Reading: The Predicate-Logic Quantifiers (up to Section 8.2) Homework 4, Deadline: October 18, 2017, 11:59pm US Central
U: Oct 12	Algebra [Z3 examples]	Reading: Circuits that Compute on Numbers: Algebra Propositional Logic as Predicate Logic [examples: #1, #2] Predicate Logic Exercise
T: Oct 17	Exam 1 Discussion Introduction to Programming Logic [examples: intro-*.logika]	Reading: Programming Logic for Assignments and Conditionals (up to Section 4.1)
U: Oct 19	Programming Logic for Assignment [examples: assignment-*.logika]	Reading: Programming Logic for Assignments and Conditionals (up to Section 4.1)
T: Oct 24	Programming Logic for Conditionals and Loops [conditional #1, conditional #2, loop #1, loop invariants recipe]	Reading: Programming Logic for Assignments and Conditionals (Section 4.2) Homework 5, Deadline: November 1, 2017, 11:59pm US Central
U: Oct 26	Programming Logic for Conditionals and Loops [loop #2, auto, symexe]	Reading: Loop, Invariants, Induction
T: Oct 31	Sequences [examples sequence-*.logika: manual, auto, symexe] Review for Exam 2
U: Nov 2	No Lecture	Instructor Office Hours: Wed, Nov 1, 1-3pm
T: Nov 7	Exam 2 [references, study guides]	Homework 6, Deadline: November 17, 2017, 11:59pm US Central
U: Nov 9	Functions and Procedures [examples: procedure-*.logika]	Reading: Functions and Procedures
T: Nov 14	Functions and Procedures [examples: procedure-*.logika]	Reading: Functions and Procedures
U: Nov 16	Global Invariants [examples: global-inv-*.logika, java] Exam 2 Discussion	Reading: Functions and Procedures
Thanksgiving Break
T: Nov 28	Exam 2 r	Homework 7, Deadline: December 10, 2017, 11:59pm US Central
U: Nov 30	Recursion [examples (manual): recursion-*.logika]
T: Dec 5	Termination [examples: termination-*.logika, Collatz: .logika, .java]
U: Dec 7	Closing Remarks Review for Final Exam
T: Dec 12	Final Exam, Time: 2:00pm - 3:50pm [references, study guides]