unicode_fol_kit.is_modal_valid

unicode_fol_kit.is_modal_valid(formula, frame='K', systems=None, max_worlds=400, max_steps=200000)

Return True iff formula is modally valid over frame — ¬formula closes.

Sound: only the closed tableau yields True. An open or bound-exhausted search yields False (the formula is then invalid-or-unknown; modal_decide() distinguishes the two with a verified counter-model).

Parameters:

• formula (Node)

• frame (str)

• max_worlds (int)

• max_steps (int)

Return type:

bool