Module kripke 

Kripke Semantics Lowering Pass

Transforms modal operators into explicit possible world semantics:

• Diamond P (force <= 0.5) → Exists w’(Accessible(w, w’) And P(w’))
• Box P (force > 0.5) → ForAll w’(Accessible(w, w’) Implies P(w’))

Structs

KripkeContext

Context for tracking world variables during Kripke lowering.

Functions

apply_kripke_lowering

Apply Kripke lowering to transform modal operators into explicit world quantification.