unicode_fol_kit.qml_is_valid

unicode_fol_kit.qml_is_valid(formula, mode='constant', frame='K', systems=None, timeout=10000)[source]

Return True iff formula is QML-valid under mode / frame (via Z3).

systems optionally sets the agent-indexed epistemic / doxastic frame systems, e.g. systems={"epistemic": "S5"} makes knowledge factive so ∀x (K_x φ → φ) comes out valid.

Sound but bounded-incomplete: True means Z3 proved validity; False means it did not (a genuine countermodel, or — since first-order modal logic is undecidable — an instance Z3 could not close). For a definite countermodel use unicode_fol_kit.semantics.kripke.satisfies_modal() over an explicit model.

Parameters:
Return type:

bool