alexhkurz.github.io

Logic in Computer Science

Compared to other disciplines such as mathematics and physics, computer science is still a young field. With the amazing technical advances we have seen, it is not a surprise that we still need to develop the computer science mathematics that will adequately support the engineering of secure and reliable software.

As a first rough approximation, one may say that logic is to computer science what mathematics is to physics.

Conversely, computer science is having a huge influence on logic. I didn’t try to count for myself, but I think it is safe to say that the vast majority of logicians nowadays is employed in computer science departments. By the way, one of them co-authored the graphical novel Logicomix in which Bertrand Russell and the history of logic are the main protagonists (highly recommended).

The best known applications of logic to computer science are probably still in hardware design (digital circuits), dating back to Shannon’s Symbolic Analysis of Relay and Switching Circuits from 1937.

But current research in logic is driven more by applications to programming and software engineering. These applications led us from the one universal logic which Russell was still seeking at the beginning of the 20th century to a large zoo of bespoke logics, each with its own applications and algorithms.

The reason why we need so many logics is in its essence contained in Turing’s famous result that the so-called halting problem cannot be solved by an algorithm, or, in more technical terms, is undecidable. In fact, a corollary of the unsolvability of the halting problem is Rice’s theorem saying that all non-trivial semantic properties of programs are undecidable.

To deal with this undecidability, several strategies have been employed:

This line of research has been very successful and gave rise to a wide range of logics and software tools, many of which are nowadays mature enough so that they can be used by programmers who did not specialise in logic.

Logic Research Area Example Tools
propositional logic SAT-solving MiniSat
temporal logic model checking SPIN
Hoare logic static program analysis Dafny
description logic knowledge representation OWL
first-order logic data base query languages SQL
logic programming Prolog
automated theorem proving Vampire
type theory interactive theorem proving Lean

Each of these logics comes in many variations, many of which fall under the broader umbrella of modal logic, a beautiful and thriving research area in its own right. Each of these research areas are big enough to spend a life-time of research in it. I would expect a student who takes a course on logic in computer science to know about SQL and maybe Prolog and OWL. But all of these tools are worth knowing. And all of them are based on implementing some kind of logical reasoning.

If you are a student at Chapman with an interest in logic, let me know. For example, I’d be more than happy to teach a course about (a subset of) the table above. There is also the possibility to do a project, for example on how to use one of the tools above in order to solve a practical problem of interest. If you are a maths student, there are also purely theoretical problems to consider.