- Instructor: Madhusudan Parthasarathy
- When: 3:30pm - 4:45pm Tuesday/Thursday
- Where: Room 1302 Siebel Center
- CRN: 49190 (3 hours) and 49191 (4 hours)
- Newsgroup: news.cs.uiuc.edu -> class.498mp
- Office Hours: Thursdays 2pm-3pm
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 first-order and second-order logic, connections between monadic second order logic and regular languages (word and tree, finite and infinite), interpretations, decidable logics using finite model properties and interpretations, finite model theory and descriptive complexity, combinations of decision procedures. The course will also cover a number of efficiently decidable logics and overview the exciting new automatic theorem provers (SMT solvers) that can reason with these logics effectively.
Prerequisite: Mathematical maturity and some knowledge of automata theory and propositional logic required.
The course will be closely modeled after the 498MV course by Mahesh Viswanathan given last year, except for a few changes:
- There will be slightly less focus on Courcelle's theorem and less focus on EF games.
- There will be instead more focus on how to use interpretations to obtain decidable logics.
- We will also study quantifier elimination for first-order logic on reals.
- We will also study how to combine decision procedures (Nelson-Oppen style), and see examples of combined theories that are decidable. We will also overview automatic theorem provers (SMT solvers) that solve combinations of theories driven by a SAT solver (such as Microsoft Research's Z3 theorem prover).
- There will be a lecture on modern applications of decidable logics, including its use as a specification logic for software (Hoare logic), its use in program verification (to decide invariants), its use in proof-carrying code, and its role in defining query languages in databases.
- See the earlier course (topics, lectures, references, etc.) to get an idea of what this course will be like.