Position paper for the 21st Century Engineering Consortium Workshop:

Moshe Y. Vardi
Rice University
February 1998

Logic as Calculus

     Logic is the foundations of formal methods. In fact, logic has been
called ``the calculus of computer science''. The argument is that logic
plays a fundamental role in computer science, similar to that played by
calculus in the physical sciences and traditional engineering disciplines.
Unlike calculus, however, the central place of logic in the computer
science curriculum is far from universally accepted. For example, the
ACM/IEEE Computing Curricula1991 lists logic only as one of many
mathematics requirements. Yet logic plays an important role in areas of
Computer Science as disparate as architecture (logic gates), software
engineering (specification and verification), programming languages
(semantics, logic programming), database (relational algebra and SQL),
artificial intelligence (automatic theorem proving), algorithms (complexity
and expressiveness),and theory of computation (general notions of
computability).  Central notions of computer science are part and parcel of
logic: abstraction and encapsulation, syntactic entities as objects of
discourse, precise syntactic rules and operations, and the dichotomy of
syntax and semantics. Some might even argue that much of computer science
can be seen as a generalization or outgrowth of logic.

    Logic can be viewed a (relatively) simple formal language that can be
used to introduce computer scientists to formal reasoning in software and
hardware design. It should be presented to computer scientists as the
conceptual underpinning of computer science itself. In an ideal world where
resources are plentiful there should be an upper division undergraduate
course on logic in computer science. In reality, however, many CS
departments can not afford to have such a course in their undergraduate
curriculum. What is to be done, then? There are plenty of opportunities to
cover a fair amount of logic in several undergraduate courses (both lower
division and upper division ones)and tie this material to concrete
applications.

     Here are three such courses:

* Introduction to CS:
In a general introduction to CS for non-majors or pre-majors, one can cover
the basics of propositional logic and relate it to gates, circuit design, etc.

* Discrete Mathematics:
A thorough treatment of propositional logic should be presented in this
course.

* Database Systems:
This course provides an excellent opportunity to present the basics of
first-order logic in the guise of relational calculus and show how SQL is
essentially a first-order language.


     Logic in computer science should be taught, however, from the computer
science perspective. Using traditional mathematical logic courses,
supplemented with minor computer-science related afterthoughts, misses the
mark and merely alienates those students who have no particular interest in
mathematical logic as such.  Thus, there needs to be a strong emphasis on
algorithmic aspects. For example, unique readability should be taught also
as a parsing issue, propositional satisfiability should be connected to
NP-completeness, provability should be viewed as polynomial-time
checkability, and undecidability should be emphasized over incompleteness.


     Formal methods, however, can be taught without requiring the students
to take an advanced logic course. At Rice, we have successfully taught
undergraduate students in computer science and engineering an applied
computer-aided verification course, without requiring anything more
advanced than  a discrete math course and an algorithm course. I will
report on our experience with such a course.