On the Unusual Effectiveness of Logic in Computer Science by Halpern, Halper, Immerman, Kolaitis, Vardi, and Vianu
The authors of these papers are well-renowned authorities in the area of logic in computer science, each with his own enormous contribution to the area.
Here is a summary of the paper. The authors start by mentioning two attempts of explaning the unreasonable effectiveness of mathematics in natural sciences by E.P. Wigner, a Nobel Laureate for Physics, and R.W. Hamming, an ACM Turing Award (which can be construed as the Nobel Prize for Computer Science) winner. In their separate papers, Wigner and Hamming give a number of examples supporting his argument, but conclude that the question "Why is mathematics so unreasonably effective" remains open. The above paper by Halpern et al. is basically an attempt to answer the question "why logic is so effective in computer science". Like Wigner and Hamming did, Halpern et al. give a number of examples supporting their assertion:
- Example 1: Descriptive Complexity. The reader should know roughly what this is by now.
- Example 2: Logic as a Database Query Language. This area is devoted to the study of abstract query languages in database theory. Examples of abstract query languages are relational calculus (equivalent to first-order logic), and conjunctive queries (see here for a definition).
- Example 3: Type Theory in Programming Language Research. Type theory is often used for building useful type systems for strongly-typed programming languages including Haskell (the computer science reader should know that C, for example, is not strongly-typed).
- Example 4: Reasoning about Knowledge. You may think of this area as "the theory of agents". Reasoning about knowledge plays a key role in burgeoning computer science fields including distributed computing, game theory, and AI.
- Example 5: Automated Verification in Semiconductor Designs. The meaning is self-explanatory.
Aside: I would love to see proof complexity and bounded arithemetic discussed in this paper.
Incidentally, Halpern et al. make a very interesting remark in their paper --- that logic seems more connected to computer science than to mathematics. To a theoretical computer scientist like myself, this claim is so conspicuous. I'm curious whether philosophers and/or mathematicians and/or logicians think so too ...