Documentation

Complexitylib.DescriptiveComplexity.ModelChecking

Computable first-order model checking #

Over a finite structure the quantifiers of first-order logic range over a finite universe, so satisfaction is decidable. This module gives a Bool-valued evaluator Formula.evalB over a decidable structure (DecFinStruct) and proves it agrees with the propositional Sat/Models.

Computable FO model checking supports the planned machine proofs of Fagin's theorem and the Immerman–Vardi characterization. SecondOrder.ModelChecking extends it to FO matrices with supplied relation witnesses. The nonuniform FO ⊆ AC⁰ inclusion is proved by finite quantifier expansion in DescriptiveComplexity.AC0. ModelChecking.PolynomialTime proves that each fixed sentence's encoded verdict is in FP and its query language is in P.

Main definitions and results #

source
def Complexity.DescriptiveComplexity.Formula.evalB {V : Vocabulary} (A : DecFinStruct V) {n : Nat} :
Env A.card n → Formula V n → Bool

Computable Bool-valued first-order model checking over a decidable finite structure: quantifiers range over the finite universe Fin card via List.finRange.

Equations
Instances For
    source
    theorem Complexity.DescriptiveComplexity.Formula.evalB_eq_sat {V : Vocabulary} (A : DecFinStruct V) {n : Nat} (φ : Formula V n) (σ : Env A.card n) :
    evalB A σ φ = true ↔ Sat A.toFinStruct σ φ

    FO model checking is correct: the Bool evaluator agrees with satisfaction.

    source
    def Complexity.DescriptiveComplexity.Sentence.evalB {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) :
    Bool

    Model checking of a first-order sentence on a decidable structure.

    Equations
    Instances For
      source
      theorem Complexity.DescriptiveComplexity.Sentence.evalB_eq_models {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) :
      evalB A φ = true ↔ Models A.toFinStruct φ

      Sentence model checking is correct.

      source
      @[instance_reducible]
      instance Complexity.DescriptiveComplexity.decidableModels {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) :
      Decidable (Sentence.Models A.toFinStruct φ)

      First-order truth over a finite structure is decidable (via the correct Bool evaluator).

      Equations