DIMACS Summer School on Applied Logic

Tutorial on Finite Model Theory

Tentative Schedule and Syllabus

Daily Schedule and Timetable, Monday through Friday
9:00-10:30 Track A: Expressive Power of Logics (Kolaitis)
10:30-11:00 Coffee Break
11:00-12:30 Track B: Descriptive Complexity (Immerman)
12:30 - 2:30 Lunch Break
2:30 - 4:00 Track C: Random Finite Models (Lynch)
4:00 - 4:30 Coffee Break
4:30- 5:30 "Office hours" and free discussion

  • Monday, August 14

    •    A. Introduction to finite models:
      First-order logic,  Second-order logic
      Monadic existential second-order logic (monadic NP)
      Ehrenfeucht-Fraisse games for first-order 
         and second-order logic

   B. Introduction to descriptive complexity:
      Complexity classes and complete problems
      FO is contained in LOGSPACE
      Fagin's theorem: "NP = Existential Second-Order Logic"

   C. Introduction to random models:
      Measures of size: cardinality and probability
      Countable structures and first-order logic:
        back-and-forth game
        Gaifman's 0-1 law 
      Finite relational structures and first-order logic:
        0-1 law of Fagin and Glebskii et al.

  • Tuesday, August 15

    •     A. Lower bounds for expressibility in monadic NP
       (connectivity is not expressible in monadic NP)
       Least fixed point logic LFP: syntax and semantics
       Existential least fixed point logic and Datalog

    B. Descriptive complexity on ordered finite models:
       PTIME = (FO + LFP)     (Immerman-Vardi Theorem)
       NLOGSPACE = (FO + TC)  (Transitive Closure Logic)
       LOGSPACE  = (FO + DTC) (Deterministic Transitive Closure 
          Logic)
       Space Complementation Theorem 

    C. Structures with built-in relations and first-order logic:
         Convergence law for structures with built-in successor
       Random graphs:
         Cases where the 0-1 law holds

  • Wednesday August 16

    •      A. Stage comparison theorem for least fixed point logic
        Immerman's complementation theorem 
        Stratified Datalog vs. least fixed point logic
	Inflationary fixed point logic IFP

     B. Parallel machines and Iterating Formulas:
        (FO + LFP) = FO[n^{O(1)}]
        CRAM[t(n)] = FO[t(n)]  (parallel time equals quantifier 
           depth)
        FO = CRAM[1] = AC^0

     C. Analytic methods:
        Generating functions and their applications to finite 
           model theory
        0-1 laws from generating functions

  • Thursday August 17

    •      
     A. Partial fixed point logic PFP
        Finite Variable Logics 
        k-pebble games for finite variable logics
   
     B. PSPACE =  (FO + PFP) = FO[2^{n^O(1)}], on ordered finite 
           models
        DSPACE[n^k] = VAR[k+1]
        Lower bounds (without order):
        (FO(wo<) + TC) properly  contained in FO(wo<)[log n]

     C. Convergence laws for higher-order logics:
        Monadic second-order logic
        Finite variable logics

  • Friday August 18

    •      A. Types for finite variable logics, definability of k-types
        Abiteboul-Vianu Theorem: 
        PTIME = PSPACE if and only if LFP = PFP.
    
     B. Lower Bounds for (FO + LFP + Counting): (Cai-Furer-
           Immerman's Theorem)
        Reductions in Descriptive Complexity: 
          first-order reductions, first-order projections          

     C. Nonconvergence results:
        First-order logic of graphs with built-in linear ordering 
        Monadic second-order logic of graphs
        Finite variable logics