Logic in Computer Science


Lec#
Topic
Slides PDF/PPT
1
Course overview and logistics; 
 A brief history of logic
2
Propositional logic -- syntax and semantics; Konig's Lemma
Lecture #2 -  
    Slides (PDF) 
    Printable (PDF)
3
Proof systems for propositional logic: 
  Resolution proof system, 
  A Hilbert/Frege style proof system, 
  Soundness of these systems
Lecture #3 - 
    Slides (PDF) 
    Printable (PDF)
4
Propositional logic: 
  Hintikka's lemma, 
  Model-existence theorem
Lecture #4 -  
     Slides (PDF) 
     Printable (PDF)
5
Compactness theorem: 
    Two proofs: One using Model-existence theorem; 
        one using Konig's lemma.

Lecture# 5: 
    Lost due to computer crash!
6
Propositional Consequence/Strong Completeness Theorem 
   for Resolution. 
The Advent of SAT solver technology: history, DPLL, conflict clause 
learning, and modern SAT solvers.
Lecture #6: 
Strong Completeness:  
     Slides (PDF) 
     Printable (PDF)
7
Review of automata theory, computability and complexity theory. 
Cook-Levin theorem (SAT is NP-complete) and its proof.
Lecture #7: 
Review of automata, computability and complexity 
(Mahesh's notes): 
    Slides (PDF) 
    Printable (PDF) 

Cook-Levin Theorem and some 
 interesting complexity 
 theory results: 
    Slides (PDF) 
    Printable (PDF)
8
First-order logic: Syntax and semantics; 
 Equality
Lecture #8: 
    Slides (PDF) 
    Printable (PDF)
9 
10
First Order Logic: 
   Hintikka's Lemma 
   Model-existence Theorem 
   Resolution: Soundness & Completeness
Lectures #9 and #10: 
    Slides (PDF) 
    Printable (PDF)
11
Church-Turing Theorem: 
   Validity of FOL is undecidable. 
Godel's incompleteness theorem (first)
Lecture #11: 
    Slides (PDF) 
    Printable (PDF)
12 
13
Second-order logics 
 Monadic second-order logics 
 MSO over words and Regular Languages
Lecture #12 and #13: 
    Slides (PDF)
14
Interpretations: 
   Deciding FOL(N,+,0,1) by interpretation 
          on MSO(N, succ). 
   Deciding FOL over infinite trees by 
          interpretation on MSO(N, succ)
Lecture #14: 
    Slides (PDF)
15
Monadic Second Order Logic 
   on finite trees 
 MSO and regular tree languages  
 MSO on infinite trees; 
 Rabin's theorem: 
   MSO over infinite trees is decidable
Lecture #15: 
    Slides (PDF)
16
Decidability of emptiness of tree automata; solving finite-state games; brief sketch of checking emptiness of automata on infinite trees.
Lecture #16: 
   Slides (PDF) 
17
MSO interpretations: 
  Decidability of MSO on n-ary trees; 
  Decidability of MSO on series-parallel 
       graphs.
Lecture #17: 
   Slides (PDF)
18
More interpretations: 
 Decidability of MSO on pushdown graphs 
 Decidability of FO on automatic graphs 
    (part 1)
Lecture #18: 
   Slides (PDF)
19
Decidability of FO on automatic graphs (part II) 
 FO of reals with addition and multiplication 
   is decidable (Tarski) 
 Quantifier elimination 
Lecture #19: 
   Slides (PDF)
20
Finite model theory I: 
   Review of classical logic. 
   Failiure of fundamental theorems in finite model theory: 
compactness theorem fails, valid sentences not in r.e.        (Trakhtenbrot's theorem) 
The three themes: 
   1. Logic and compexity theory 
   2. (In)expressivess of logics, EF games 
   3. Classical theorems reevaluated in 
          the finite model setting.
Lecture #20: 
   Slides (PDF)
21  
22
Finite model theory: 
   Ehrenfeucht-Fraisse Games 
   Quantifier rank 
   EVEN not expressible in FOL 
   CONNECTED not expressible in FOL 
   Proof of EF-theorem; Rank-k types 
    
Lecture #21 & #22:  
   Slides (PDF)
23
Finite model theory: 
   - Fagin's theorem  ESO=NP
Lecture #23:  
   Slides (PDF)
24
Finite model theory: 
   - Fagin's theorem continued 
   - Fixed point logics 
        * Monotonic & inflationary operators 
        * FO + LFP
Lecture #24: 
   Slides (PDF)
25
Finite model theory (concluding) 
    - FO+LFP = P (no proof) 
    - FO+PFP = PSPACE (no proof) 
    - EMSO notequals AMSO on structures 
                         (no proof) 

Courcelle's theorem: 
    - Embedding graphs in trees 
         (examples) 
    - Definition of tree-width

Lecture #25:  
   Slides (PDF)
26
Fixed-parameter tractability 
Courcelle's theorem 
  - Any MSO property on finite graphs of 
      bounded tree-width can be 
      model-checked in linear time. 
Lecture #26:  
     Slides (PDF)
FALL BREAK - NO CLASS

FALL BREAK - NO CLASS

27, 28
Review of topics and results; 
Also SMT solvers
Lecture #27, Lecture #28 
      Slides (PDF)

No comments: