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 
           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 
            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 
            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