DEPARTMENT OF COMPUTER SCIENCE COLLOQUIUM SERIES
David Gries, Cornell University
Teaching a Useful Logic
Wednesday, March 17, 2010, 12:30pm, Xerox Auditorium
ABSTRACT
The typical discrete math course in computer science teaches a
propositional (and perhaps predicate) logic that is not used by
mathematicians (or almost anyone) in their day-to-day work. Students
come away with the idea that logic is not really useful, that it is just
an academic thing. And they certainly don't come away with the ability
to develop proofs. This can be changed by teaching Calculational Logic,
which has as its basis substitution of equals for equals rather than
modus ponens. This logic actually formalizes how a lot of mathematical
proofs are done. Further, one can teach students principles and
strategies for developing proofs, so that they DO develop a skill in
proving things. Further, one can then use calculational logic to teach
set theory, theory of arithmetic, solving recurrence relations,
functions and relations --all the major topics of discrete math.
Students can come away thinking that proof is the concept that underlies
and ties together all the topics of the course. And they like it!
BIOGRAPHY
A native of New York, Gries received his doctorate in math from MIT
(Munich Institute of Technology) in 1966. After 3 years at Stanford, he
moved to CS at Cornell, where he has been ever since, except for a few
years at UGA.
Gries is known for his research in compiling and in programming
methodology, and he has been teaching programming for over 43 years. He
wrote the first text in compiling (1971), the first programming text
that dealt seriously with loop invariants (1973, with Dick Conway), the
first undergrad text on the science of programming (1981), the first
discrete math text that makes logic and proof the underlying theme and
teaches the development of proofs (1993, with F.B. Schneider), and the
first text to come on a CD with 250 recorded lectures with synched
animation (2003, with son Paul).
Gries received national/international awards for his contributions to
education and research from AFIPS, ACM SIGCSE, ACM, IEEE Computer
Society, and the CRA, as well as two honorary doctorates.