Formal Methods: MATH 220 (3)
Formal logic as a tool for mathematical proofs. Propositional calculus—Boolean expressions, logic connectives, axioms, and theorems. Predicate calculus—universal and existential quantification, modeling English propositions. Application to program specification, verification, and derivation.
| Hours | Topic |
|---|---|
| Preliminaries (3 hours) | |
| 1.5 | Textual substitution |
| 1.0 | Leibniz rule and function evaluation |
| 0.5 | The assignment statement |
| Boolean Expressions (5 hours) | |
| 1.5 | Syntax and evaluation of boolean expressions |
| 0.5 | Equality vs equivalence |
| 1.0 | Satisfiability, validity, and duality |
| 2.0 | Modeling English propositions |
| Propositional Calculus (6 hours) | |
| 1.0 | Equational logic and inference rules |
| 0.5 | Equivalence |
| 1.0 | Negation and inequivalence |
| 2.0 | Disjunction and conjunction |
| 1.5 | Implication |
| Proof Techniques and Applications (4 hours) | |
| 1.0 | Monotonicity, deduction theorem, case analysis |
| 0.5 | Proof by contradiction |
| 0.5 | Proof by contrapositive |
| 2.0 | Solving word problems |
| Quantification (4 hours) | |
| 0.5 | Types |
| 1.0 | Syntax and interpretation of general quantification |
| 1.5 | General quantification axioms |
| 1.0 | Quantification range theorems |
| Predicate Calculus (5 hours) | |
| 1.5 | Universal quantification |
| 1.5 | Existential quantification |
| 2.0 | Formalizing English statements |
| Predicates and Programming (8 hours) | |
| 2.0 | Specification of programs |
| 2.0 | Reasoning about the assignment statement |
| 2.0 | Calculating parts of assignments |
| 2.0 | Conditional statements and expressions |
Total: 35.0 hours, excluding holidays, review sessions, and exams
*Fifty-minute class hours