CIS 301 Logical Foundations of Programming
-------------------------------------------------------

1. Prerequisites by topic:

• college algebra
• basic imperative programming skills
• intuitive understanding of the semantics of simple imperative programs
• an exposure to invariants of while-statements

2. Knowledge and skills acquired in this course:

• Mastery

1. proving propositional logic sequents in the natural deduction calculus

2. understanding syntax and truth table semantics of propositional logic

3. developing the ability to apply mathematical induction

4. proving predicate logic sequents in the natural deduction calculus

5. understanding the syntax and semantics of predicate logic

6. verifying the partial, or total, correctness of Hoare triple over a simple imperative core language

7. computing insightful invariants for while-statements
     

• Familiarity

1. converting a propositional logic formula into an equivalent formula in conjunctive normal form and appreciating its complexity

2. appreciating the concepts of "satisfiability" and "validity" of propositional logic and predicate logic formulas

3. realizing the significance of soundness and completeness of natural deduction for propositional logic and predicate logic

4. realizing the impact of the undecidability of validity and satisfiability in predicate logic

5. understanding the importance of soundness and relative completeness of proof calculi for partial and total program correctness

6. realizing the significance of the undecidability of the Halting problem

7. being exposed to a case study of algorithm design and verification