CIS 301. Captain's Log: Logical Foundations of Programming, Spring 2001.

May 11: The FINAL EXAM will be held on Friday, May 11, from 04:10 - 06:00 P.M. in Nichols 122. This is an open book exam. A template for the final exam is specified in the review.
May 4: Study period (no class).
May 2: Handouts: Solutions for Assignment #12, Graded Assignment #12. Review Assignment #12.
April 30: Review for Exam #3 (aka "The Final Exam").
April 27: Handouts: Graded Assignment #11. Collect Assignment #12. Review Assignment #11. Total program correctness for the Factorial program. Program termination: generating prime numbers.
April 25: Handouts: Solutions for Assignment #11. Correctness of the minimal-sum program. Comment on preconditions other than "T".
April 23: Hand out and review graded Exam#2.
April 20: Collect Assignment #11. Hand out Assignment #12. More example proofs of partial correctness. Total correctness proofs of programs with while-statements. Program termination: 3n+1 Collatz.
April 18: Exam #2. Four problems worth 25 points each: (i) For a predicate logic formula, (a) draw its parse tree, (b) determine its free and bound variables, (c) compute a substitution, (d-e) determine whether "t" is free for "x" in "phi". (ii) Prove a predicate logic sequent in natural deduction. (iii) Given a model of predicate logic, explain why a formula holds/doesn't hold in that model. (iv) Express an English sentence in predicate logic.
April 16: Hand out Graded Assignment #10. Review Assignment #9 and Assignment #10. Invariants. Partial correctness proofs of programs with while-statements.
April 13: Proving correctness of programs with assignments and if-statements. Invariants. Proof rule for while loops. Partial and total correctness.
April 11: Handouts: Solutions for Assignment #8, Solutions for Assignment #9, Graded Assignment #9, Assignment #11. Collect Assignment #10. An introduction to program correctness proofs.
April 9: No class.
April 6: No class.
April 4: No class.
April 2: TEVAL. Review for Exam #2. Hand out Graded Assignment #8.
March 30: Collect Assignment #9. Fixed-point characterization of CTL. The temporal logic LTL. (Solutions #7, Ex. 2.5 2(b) was flawed, corrected in last class, and the correct solutions can be found on the backside of Solutions #6. All students will get an updated score for their Homework #7: new_score = max(10, old_score + 2).)
March 28: Hand out Assignment #10. Review Assignment #7. Crossing the Mississippi.
March 26: Hand out Graded Assignment #7. Collect Assignment #8. Fairness in SMV. Verifying the Mutex Protocol.
March 23: Student Holiday.
March 21: Student Holiday.
March 19: Student Holiday.
March 16: Handouts: Assignment #9. Semantic equivalences. Three attempts of designing and verifying a mutual-exclusion protocol.
March 14: Handouts: Solutions for Assignments #6 and #7. Review of Assignment #6. More example model checks.
March 12: Handouts: Graded Assignment #6. Exam #1. Collect Assignment #7. Review Exam #1.
March 9: Exam #1.
March 7: Handouts: Assignment #8. Motivation and introduction to model checking: example model, syntax of CTL, example model checks.
March 5: Review for Exam #1.
March 2: Handouts: Graded Assignment #5, Solutions for Assignment #5. Collect Assignment #6. Predicate logic: models and semantics, semantic entailment, validity (is undecidable), soundness and completeness, incompleteness results.
February 28: Handouts: Assignment #7. Example proofs for that assignment.
February 26: Predicate logic: more example proofs, quantifier equivalences.
February 23: Handouts: Graded Assignment #4, Solutions for Assignment #4. Collect Assignment #5. Review Assignment #4. "Free for x in Phi". Proof rules for universal and existential quantifiers, more example proofs.
February 21: Handouts: Assignment #6. Predicate logic: free and bound variables, substitution, proof rules for universal quantifiers, an example proof.
February 19: Review Assignment #3. More specifications written in predicate logic. More on the syntax of predicate logic.
February 16: Collect Assignment #4. Structural induction. Introduction to predicate logic. Its syntax: terms and formulas. Writing specifications in predicate logic.
February 14: Handouts: Solutions for Assignment #3, Assignment #5. Mathematical induction: the principle, and some working examples: ex.#4 and #5 on page 56; correctness proof of NNF algorithm. Exam #1 will feature: (i) two proofs in natural deduction; (ii) determining whether a formula is satisfiable or valid; (iii) computing the conjunctive normal form of a formula; (iv) proof by mathematical induction.
February 12: Handouts: Graded Assignments #2 and #3, Solutions for Assignment #3, Assignment #5. Review Assignment #2.
February 9: Uups.
February 7: Handouts: Solutions for Assignment #2. Collect Assignment #3. How to convert a formula into conjunctive normal form: examples.
February 5: Handouts: Assignment #4. Semantic equivalence. Literals. Conjunctive normal form: syntax, connection to validity. Converting a formula into conjunctive normal form. ,Please read pages 69-83 in your text book by February 7.
February 2: Handouts: Graded Assignment #1, Solutions to Assignment #1. Review Assignment #1. Satisfiability. Validity. Sequents as validity problems.
January 31: Collect Assignment #2. Handouts: Assignment #3. Semantics of propositional logic. Soundness & Completeness.
January 29: More example proofs in natural deduction. Parse trees of logic formulas. Subformulas. Truth tables.
January 26: Collect Assignment #1. Natural deduction rules for negation. Derived rules. Law of the excluded middle.
January 24: Handouts: Assignment #2. Natural deduction rules for negation.
January 22: Natural deduction rules for implication-introduction, disjunction. The "copy rule".
January 19: What are arguments? Syntax and binding priorities of propositional logic. Natural deduction rules for conjunction, double-negation, implication-elimination, the MT rule.
January 17: Handouts: Syllabus, Errata, Assignment #1, Course prerequisites and expected outcomes. Introduction to the course, its organization, prerequisites, and objectives. (Please read pages 1-12 for next class.)

Michael Huth (huth@cis.ksu.edu)