The Tableau Game (Section 6.2 and 6.3)

Defining the Tableau Game (Section 6.2)

def Rule : Type

Equations

• Rule = ((X : Sequent) × (B : List Sequent) × LocalRuleApp X B ⊕ (X : Sequent) × (Y : Sequent) × PdlRule X Y)

def termProver : Lean.ParserDescr

Equations

• termProver = Lean.ParserDescr.node `termProver 1024 (Lean.ParserDescr.symbol "Prover")

def termBuilder : Lean.ParserDescr

Equations

• termBuilder = Lean.ParserDescr.node `termBuilder 1024 (Lean.ParserDescr.symbol "Builder")

def tableauGame : Game

Equations

• tableauGame = { Pos := Sequent ⊕ Sequent × Formula × Rule, turn := sorry, moves := sorry, bound := sorry, bound_h := tableauGame._proof_1 }

theorem gameP (X : Sequent) (s : Strategy tableauGame Prover) (h : winning (Sum.inl X) s) : Nonempty (Tableau [] X)

If Prover has a winning strategy then there is a closed tableau.

From winning strategies to model graphs (Section 6.3)

theorem strmg (X : Sequent) (s : Strategy tableauGame Builder) (h : winning (Sum.inl X) s) : ∃ (WS : Finset (Finset Formula)) (mg : ModelGraph WS), X.toFinset ∈ WS

If Builder has a winning strategy then there is a model graph.