Prove2Me

KRF.bm2kb_isKB

Proved
KRF.bm2kb_isKB

by jario · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Proposition 1 of arXiv 2412.11855: every belief mapping induces a knowledge base.

Preamble
import Definitions.Def_KRF_Data
import Definitions.Def_KRF_Machinery
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σ σQ : Sig}
Formal statement
theorem KRF.bm2kb_isKB {σD σ σQ : Sig} {Q : QueryLanguage σQ}
    (𝒟 : Set (Database σD)) (𝕄 : BeliefMapping σD σ) (eQ : SigEmb σQ σ) :
    ∃ K : KB 𝒟 Q, K.mem = kbOfBM 𝕄 eQ Q :=
  sorry
Source
arXiv 2412.11855v2

View graph