[Prev][Next][Index][Thread]

Need recommendation for "Logic for CS" text

[Please reply directly to the poster, not to Types.  Josh, could you
summarize the replies here in a few days?  --BCP]


I know this is the types list, not the logic list, but I suspect your
views on logic coincide more with mine, so it seems a better place to
ask.

I have convinced my department (CS) that we should have an
introductory "logic for CS" course required in our major and taken at
the sophomore level. I will be teaching this course for the first time
next semester and am looking for your suggestions as to a good text
for such a course.

The students in the course will, as I said, be mostly sophomores.
They will have had four or more semesters of calculus (we require 2
for entry to the school), and a semester of discrete math, so they are
relatively mathematically sophisticated. They will also have had one
or more semesters programming in Java / C++, and a semester course
that covers a broad variety of CS concepts including a bit of
functional programming, parsing, logic design, architecture/assembler,
etc.

The goal is to concentrate on logic as applied to CS: More proof theory
than the typical math department intor, alot of examples of using FOPC 
sentences to describe a problem (i.e., AI and database applications of
FOPC), mostly Gentzen-style proof systems, with some discussion of other
styles, hopefully some presentation of intuitionistic systems and their
connections to the foundations of CS. The emphasis will not be on proofs
of the major theorems. There will be both pen & paper, and programming 
assignments. My hope is to introduce at least one proof assistant or
prover.

Can any of you recommend a good text? While the coverage in Gallier is the
right material, it is, I think a bit too intimidating in its style
(and a bit too classical, as well). Ben-Ari is less deep, but is under
considertation (particulalry because he uses Gentzen-style deduction).

Thanks in advance for any help you can profer.

Josh Hodas