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