Logic in computer science

For the academic conference LICS, see IEEE Symposium on Logic in Computer Science.

Logic in computer science describes topics where logic is applied to computer science and artificial intelligence. These include:

Investigations into logic that are guided by applications in computer science. For example: Combinatory logic and Abstract interpretation;
Fundamental concepts in computer science that are naturally expressible in formal logic. For example: Formal semantics of programming languages, Hoare logic, and Logic programming;
Aspects of the theory of computation that cast light on fundamental questions of formal logic. For example: Curry-Howard correspondence and Game semantics;
Tools for logicians considered as computer science. For example: Automated theorem proving and Model checking;
Logics of knowledge and beliefs (of human and artificial agents);
Logics for spatial reasoning, e.g. about moving in Euclidian space (which should not be confused with spatial logics used for concurrent systems);
Formal methods and logics for reasoning about computation. For example predicate logic and logical frameworks are used for proving programs correct, and logics such as temporal logic and spatial logics are used for reasoning about interaction between concurrent and distributed processes. Program logics often are modal logics, e.g. dynamic logic or Hennessey-Milner logic;
Specification languages provide a basis for formal software development; in this context, the notion of institution has been developed as an abstract formalization of the notion of logical system, with the goal of handling the "population explosion" of logics used in computer science.

The study of basic mathematical logic such as propositional logic and predicate logic (normally in conjunction with set theory) is considered an important theoretical underpinning to any undergraduate computer science course. Higher order logic is not normally taught, but is important in theorem proving tools like HOL.