Jonathan Ostroff, Zbigniew Stachniak, Andy Mirzaian, Jeff Edmonds
Rationale for restructuring the logic and discrete maths courses for CS
MATH1090 | MATH2090 | MATH2320
The tentative proposal is to start with the new version of MATH1090 in the Fall of 1998 , and in the fall of 1999 with the new versions of MATH2090 and MATH2320. No change to the calendar need be made until we are satisfied that the proposal works. An important part of the proposal is that the students get weekly assignments in MATH1090/2090 (biweekly in MATH2320) to ensure that they become comfortable with using predicate logic to describe problems, proof strategies and discrete maths in a variety of areas.
[GS] A
Logical Approach to Discrete Maths. Gries and Schneider. Springer
Verlag. Between the text and instructor's manual there are 700 worked
out examples. The text works on the basis that logic is the glue that underlies
reasoning in all areas of Computer Science. Hence logic is treated first,
and then that logic is used in a variety of discrete domains (sets, combinatorics,
recurrence relations, graph theory etc.). A revised edition is currently
being planned. A list of errors is
available for the current edition.
[Tar] Tarski's World. Barwise and Etchemendy. CSLI publications.
Version available for Windows and Macintosh. (Comes with a tool for introducing
students to well-formed formulas, sentences and validity; there is a way
to automatically grade assignements; the tool is *not* a proof system but
a tool for introducing semantics).
[GSE] Equational Propositional
Logic. Gries and Schneider. This is a 15 page article that describes
the equational proof system [E] used in [GS] including (a) the axioms and
inference rules of [E], (b) using them Hilbert style, (c) their soundness
and completeness.
General note to instructors: The Computer Science Department would like
to see regular assignments (one per week) as well as a test and a final
exam for each course below.
General INTRODUCTION: Logical Foundations of Computer Science
a. The role of logical foundations in present-day computer science:
- Logic as a formalization language (formal specification languages,
program verification, etc.);
- Logic as an execution or programming language (logic programming,
program synthesis, abstract interpretations of specifications),
- Logic as knowledge representation language and a mechanism for
knowledge manipulation in Artificial Intelligence (knowledge
representation, automated deduction, planning, expert systems,
deductive data bases, etc.)
b. Formal Deductive Systems
- Propositions, beliefs and declarative sentences, syntax vs. semantics
- Formalization as the process of constructing an object language
together with rules (of reasoning) for manipulating sentences in the
language; formal vs natural languages
- Formal deductive systems; the notions of:
- a formalized language (alphabet and grammar or syntax
formation rules),
- axioms,
- rules of inference,
- proofs
The rest of the course outline quotes chapters from the text [GS]:
Chapter 1: [Introduction to the proof system] Textual Substitution, axioms
of equality and the 4 inference rules including Leibniz. Reasoning using
Leibniz's rule is similar to the way algebra is done in high school (substituting
equals for equals). Example application: reasoning about the assignment
statement in programs (preconditions and postconditions). Note to instructor:
please look at [GSE] for full background to the proof system.
Chapter 2: [Boolean expressions] Boolean expressions and truth tables. Equivalence
is the special equality symbol when the types of the operands are boolean.
Equality is used conjunctively whereas equivalence is used associatively.
Satisfiability. Modelling English propositions. Note to instructors: a small
number of propositional exercises in [Tar] can be done at this point.
Chapter 3: [Propositional Calculus] Proving theorems in the proof system.
Note to instructors: students should be asked to do a large number of proofs
in the proof system at this point.
Chapter 4: [Proof strategies] Relaxing proofs, the deduction theorem, proof
by cases, proof by contradiction, and proof by contrapositive. Students
should be asked to do some proofs in each category (see instructors manual).
Note to instructor: see JSO for notes from authors of how to do monotonic
proofs better. An advantage of natural deduction techniques is that it gets
students used to doing conditional proofs. The equivalent in GS has to be
done using the deduction theorem.
Chapter 5: Applications of propositional calculus. Do a few examples of
cominational digital circuits. The proof system can be used to demonstrate
that a digitial circuit implements a specification. Note to instructor:
don't spend too much time here, but it is a nice application for propositional
logic.
Chapters 6 and 7: [Hilbert style proofs and formal logic.] Note to instructors:
the text does this poorly. Instead use [GSE] for Hilbert style proofs. Use
[Tar] to introduce the notions of well-formed formulas, sentences and validity.
Do some propositional exercises. Use [GSE] to discuss the soundness of the
proof system used in [GS]. (The idea of completeness should be mentioned
but not proved in detail).
[Tar] can then be used to introduce the notion of existential and universal
quantifiers. Do some exercises in predicate logic from [Tar].
Chapter 8: [Quantification]. Any symmetric, associate operator can be generalized
to a quantifier. Can therefore have one uniform notation for quantification
whether it is universal, existential, summation, product, max. etc. Discuss
scope and bound and free occurences of variables. Introduce some theorems
(e.g. range split and one point rule) and use these theorems.
Chapter 9: [Predicate Calculus]. Using the proof system to do predicate
calculus. Note to instructor: do a lot of proofs at this point.
Chapter 10: [Applications of predicate calculus]. Program specfication (preconditions
and postconditions) and program verification. Note to instructor:do up to
and including ch 10.3 (assignments and sequences of assignments).
Chapter 11: [A theory of sets]. Do whole chapter. Use both Venn diagrams
as well as set theory proofs in the formal proof system. Discuss ill-defined
sets and paradoxes (ch 11.6).
Chapter 12: [Mathematical Induction]. Do only up to and including chapter
12.1: induction over the natural numbers.
This course continues where MATH1090 left off. It will use the same text
[GS] as MATH1090 and will reuse the proof system over and over again in
the various discrete domains (sequences, relations and functions, combinatorics,
recurrence relations etc.).
Chapter 12: [Mathematical Induction]. Induction over natural numbers. Inductive
definitions. Peano arithmetic. Induction and well-founded sets etc. Do some
of the program verification examples for loops.
Chapter 13: A theory of sequences.
Chapter 14: Relations and Functions.
Chapter 15: A theory of integers including reasoing with DIV, MOD, ABS,
MAX, MIN etc.
Chapter 16: Combinatorial analysis. Do whole chapter in detail.
Chapter 17: Recurrence Relations. Do whole chapter in detail.
Chapter 19: A Theory of Graphs. Do whole chapter in detail.
Chapter 18: Modern algebra.
Chapter 20: Infinite sets. Countable and uncountable sets.
MATH 2320: Discrete Mathematical Structures
TEXT BOOK:
[Ros] Kenneth Rosen, "Discrete Mathematics and its Applications"
3rd Edition, McGraw-Hill, 1994.
SUPPLEMENTARY READING:
- a source on Discrete Probability.
SUGGESTED CHANGES:
- Students should get (bi-)weekly scheduled homework assignments,
which makes up 30%-40% of the overall grade. This is a serious
concern for us.
- Discrete probability appears only in sections 4.4 and 4.5 of [Ros]
and it was completely skipped. This subject is need for many COSC
courses. We suggest to beef up the content of those section by
using supplemental reading material, and spend about 3 weeks of
the course on that topic.
- Based on the suggested changes to Math 1090/2090, certain sections
of [Ros] that are currently being taught can be skipped, or quickly
reviewed, in order that some other topics will have a more in depth
coverage. See further details below.
TOPICS COVERED:
CHAPTER 1 (1.5 weeks):
(Sections 1.6 - 1.8 & perhaps Appendices A.1,2,3):
Series sum/product: Exact, as well as asymptotics and approximation techniques.
For example using integration, summation in parts, possibly using some
techniques from Generating functions (as discussed later in Appendix A.3).
(Note: The instructor can choose to introduce the topics of the
Appendices at the appropriate time.)
CHAPTER 2 (0.5 week):
(Sections 2.1 - 2.6):
Algorithm step counting, some number theory, matrices.
-Sections 2.1 and 2.2 etc. will get more coverage in COSC.
CHAPTER 3 (1.5 weeks):
(Sections 3.1 - 3.5):
-Quickly review proof techniques.
-Spend more time on Induction (weak, strong, structural, and the principle
of minimality).
-Discuss counter-examples of plausable but false claims to reinforce the
need for careful proofs.
-Section 3.5 will get more coverage in COSC.
CHAPTER 4 (2 weeks):
(Sections 4.1-4.3 4.6-4.7 & Appendix A.3):
-counting techniques, permutations, combinations,
generating functions.
CHAPTER 4 (2 weeks):
(Sections 4.4,4.5 and Supplementary reading):
Discrete Probability.
CHAPTER 5 (1.5 weeks):
(Sections 5.1-5.5):
According to the course web page the important section 5.2 on
solving recurrence relations was skipped. More emphases should
be put on that.
CHAPTER 6 (1 week):
Sections 6.4-6.6 on closure, equivalnce relations and partial orders
should preferably be covered.
CHAPTER 7 (2 weeks):
Sections 7.1, 7.5, 7.7 at least (graphs: Euler, Hamiltonian, planar ...).
Try not to cover what is covered in Math2090 in this area.
CHAPTER 8:
Trees get sufficient coverage in earlier COSC courses.
Cover if there is time