unicode_fol_kit.announce

unicode_fol_kit.announce(model, formula)

Return model updated by a truthful public announcement of formula.

The result keeps exactly the worlds where formula is true (under satisfies_modal()); every relation is restricted to those survivors and the valuation (and per-world object domains, if any) likewise. Inputs are not mutated.

Parameters:

• model (KripkeModel)

• formula (Node)

Return type:

KripkeModel