Logical Foundation of Computer Science

Course Overview:

Logic is one of the corner stones of computer science. Logic plays a crucial role in diverse areas of computer science such as architechture (logic gates), software engineering (specification and verification), programming languages (semantics, logic programming), databases (relational databases, SQL, XML processing), artificial intelligence (automatic theorem proving, inductive reasoning), algorithms (complexity and expressiveness), and theory of computation (general notions of computability).

This course will provide an introduction to mathematical logic from the perspective of computer science, emphasizing decidable fragments of logic and decision algorithms. The topics covered will be motivated by applications in artificial intelligence, databases, formal methods and theoretical computer science. The goal of the course is to prepare students for using logic as a formal tool in computer science. The course will roughly cover the following topics (in this order): syntax, semantics and proof theory of propositional logic, sat-solvers, syntax of first-order, the resolution proof system, syntax of second-order logic, connections between monadic second order logic and regular languages (word and tree, finite and infinite), tree-width and Courcelle's theorem with applications to parametric complexity, finite model theory and descriptive complexity, games and inexpressiveness.