Summary: logic texts for computer scientists

A few days ago I asked here for recommendations of "a broad
introduction to logic 'from a computational perspective' and aimed at
nonspecialists."  I got many responses, summarized below.

The most popular suggestions were
  - various papers and a book by Jean Gallier
  - online lecture notes (draft book) by Sorendsen and Urzyczuyn
but there's lots of stuff out there, it seems!
Many thanks for all the help,



From: "R.C. McDowell" <mcdowell@kzoo.edu>

I'm not sure exactly what you're looking for in terms of coverage.  But
here are a couple of things to consider.

Jean Gallier put together some notes as an introduction to the field of
logic and computation.  These notes were published in two parts in TCS.  
The first part of the notes covers natural deduction, sequent calculus,
and the simply typed lambda-calculus in the context of the Curry-Howard
isomorphism.  The second part covers linear logic and related materials. I
only have a reference for the first part; the second part was published
significantly later (Jean can give you the reference).

Gallier, J.  Constructive Logics. Part I: A tutorial on proof systems
    and typed lambda-calculi.  Theoretical Computer Science, 110(2):
    249-239 (1993).

I've recently come across a book by Michael Downward that introduces
the logical basis for logic programming languages, functional programming
languages, and relational databases.

Michael Downward, Logic and Declarative Language, Taylor & Francis, 1998.

I've only glanced through the book so I can't say too much about it, but
I'll list the chapter titles for you.

Part I. Logic without equality
   1. Propositional logic
   2. First-order logic
   3. Principles of logic programming
   4. Prolog

Part II. Logic with equality
   5. Logic with equality
   6. Many-sorted abstract types
   7. The included middle
      (This chapter includes a discussion of the untyped lambda-calculus.)
   8. Miranda
   9. Intuitionistic logic and types
      (This chapter includes a discussion of the Curry-Howard
  10. Languages and databases


From: Daniel Leivant <leivant@cs.indiana.edu>

I have been using for some years my own lecture notes, with the
intention of having them tidy up to become a textbook.  I was planning
to work on this actively this summer.

The computer science ties i emphasize are not that much algorithmic,
as conceptual: e.g. word algebras are used as fundamental data type
rather than natural numbers.  Other expository features include: (1)
opening with "informal rigor" and "proto-semantics", rather than pure
syntax and proof rules.  (2) careful distinctions between syntax and
(various levels of) semantics.  (3) taking proofs as actual rather
than potential; thus the formalisms DO count, and equational logic is
pedagogically important because students are used to seeing formal
equational proofs.  (4) highly economical proofs of church and godel
undecidability theorems.  (5) intro to resolution, higher order logic,
dynamic logic, and Hoare-style logics.


From: Sergei Vorobyov <sv@mpi-sb.mpg.de>

Look at J. Gallier, TCS vol 110, 1993, pp 249-339

Constructive logics. Part I: A tutorial on proof systems
and typed lambda calculi


From: dezani@di.unito.it (Mariangiola Dezani)

What about the fortcoming book of Odifredi&Nerode?
I know also Sorendsen&Urzyczuyn are are writng a new book.


From: Luis Caires <Luis.Caires@di.fct.unl.pt>

I've enjoyed the following tutorial articles by Jean Gallier.
These are nice pedagogical texts I guess, you probably know them ...
the focus is on C-H. correspondence.

Constructive Logics. Part I: A Tutorial on Proof Systems
and Typed lambda-Calculi. Theoretical Computer
Science, 110(2), 249-239 (1993).

Constructive Logics. Part II: Linear Logic and Proof Nets.
Technical Report, CIS Department, University of
Pennsylvania, 1991. 

On the Correspondence Between Proofs and lambda-Terms. 
Cahiers du Centre de Logique, Philippe DeGroote, Editor,
Université              Catholique de Louvain,1995.


From: Samin Ishtiaq <si@dcs.qmw.ac.uk>

I think Gallier's 1992? notes on Constructive Logic are quite good.
They're meant as introductory material, but do cover a wealth of
topics in good enough detail. I think the notes appeared in TCS,
but I might be wrong.


From: Masako Takahashi-Horai <masako@is.titech.ac.jp>

How about a recent book by Troelstra and Schwichtenberg called
"Basic Proof Theory (Cambrige Univ. Press)"?

As another much simpler guide for real beginers, I may suggest 
my recent article,
	M. Takahashi: A primer on proofs and types,
	in "Theories of Types and Proofs" edited by 
	M.Takahashi, M.Okada, and M.Dezani (MSJ Memoirs, Vol.2, 
	Mathematical Society of Japan, 1998), pp.1-42.


From: Andrew Ian Schein <ais@seas.upenn.edu>

I am not sure this is as broad a text as you would prefer, but Philip
Wadler's article: "A taste of linear logic" served me as a
straightforward introduction to intuitionistic logic, linear logic, and
the Curry-Howard Isomorphism. And it even made me chuckle. It is hanging
off of Wadler's website: "lineartaste.ps".


From: Anton Moscal <msk@post.tepkom.ru>

may be

Lambek J., Scott P., Introduction to Higher-Order Categorical Logic

This book close to you requirements. 
Also I can recommend the following book:

Goldblatt R., Topoi, the categorial analysis of logic.

The main subject of this books is logic and its interpretation in the
category theory, but in the introductionary chapters contains very good
explanation of many categorical concepts, such as epic and monic 
morphisms, subobject, topos etc.

This is best known to me introduction in category theory and its relation
to logic (but not "from a computational perspective")

[[Having a passing familiarity with both of these books, I think
they're excellent but would not describe them as suitable for
nonspecialists!  --BCP]]


From: Frank Pfenning <fp@raw.fox.cs.cmu.edu>

My book on Computation & Deduction may be a candidate.  However, it
does not cover automated deduction, classical logic, or other
traditional material, but it does cover judgments, natural deduction,
Curry-Howard, sequents, program extraction, logical relations.  It
does all this with the help of a logical framework implementation.

One drawback: it won't be out until early next year (to be published
by Cambridge University Press).


From: Pawel Urzyczyn <urzy@mimuw.edu.pl>

How about if you try this:


This is _not_ a logic text as such but rather lambda-calculus and logic
in parallel. But perhaps may be useful to some extent (despite all the bugs
more and more of which we keep discovering). All comments are very welcome. 


From: Buday Gergely <gergoe@math.bme.hu>

Look at Sorensen and Urzyczyn's 'Lectures on the Curry-Howard Isomorphism'.
It's a report of DIKU, so go
http://www.diku.dk/ -> Research -> Technical Reports 1998
You can obtain a hardcopy of it as well.

It isn't aimed at nonspecialists, but worth looking at.


From: Luis Lamb <ldcl@doc.ic.ac.uk>

I found that Elementary Logics: a Procedural Perspective by DM Gabbay,
is a very good introductory text to Computer Scientists. It covers
many logics used in CS such as propositional logic, non-classical
(temporal, intuitionistic) logics, first-order logic, modal logic, and
non-monotonic logics, all from a procedural (proof theoretical)
perspective; I think this book is really good for learning how to make
proofs and to associate logical reasoning to CS. It is also clearly
aimed at non-specialists.  


From: "Randy Pollack" <rap@dcs.ed.ac.uk>

I taught a course at BRICS, "Introduction to Logic and Formal
Systems".  My goal was to have students understand that a formal
system is a mechanism, and a technology must be mastered to use it.
Different systems have different technologies, and none of this has
much to do with "truth".  However, the concreteness of a particular
system and its technology is important; it is the source of whatever
meaning the system has.

The particular formal system I wanted the students to master was
Constructive Type Theory with inductive types; e.g. LEGO.  I started
from minimal logic, emphasising the introduction/elimination duality
and its "computation rule", beta reduction.  We moved to full
propositional logic, then first-order logic, by adding new syntax with
its new introduction/elimination/computation rules.  But this is just
raw logic (i.e. hypothetical, non-ground, hence largely
non-computational); how to get some mathematical content for
computation to work on?  Inductive types, based on the same
introduction/elimination/computation notion as for logical
constructors!  This is what is missing in all treatments I know of: we
should treat Inductive types in a first-order setting as
philosophically identical to logic.  (Here my logicist leanings are
showing.)  There is such a presentation in Martin-Lof's "Haupsatz for
the intuitionistic theory of iterated inductive definitions" in the
Second Scandanavian Logic Symposium, North Holland, 1971.  Of course
it is hard to read, and needs to be elaborated with examples for a
basic course.  Once over this step, full type theory with inductive
definitions is easy to sell.

Coming back to your question, your students may find the text by
Gallier (below) useful.

Best wishes,

  author =       "J. H. Gallier",
  title =        "Logic for Computer Science: Foundations of Automatic
                 Theorem Proving",
  publisher =    "Harper \& Row",
  year =         "1986",
  volume =       "5",
  series =       "Computer Science and Technology Series",
  address =      "New York",


From: Atsushi Igarashi <igarasha@saul.cis.upenn.edu>

>> There is, of course, the old standby -- Girard, LaFont, and Taylor's
>> Proofs and Types.  Hindley's new book (Basic Simple Type Theory) has a

It seems Proofs and Types has been out of print, unfortunately.