unicode_fol_kit.modal_decide

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

Decide formula over frame: "valid" / "invalid" / "unknown".

"valid" — the tableau for ¬formula closed (a sound proof). "invalid" — an open branch yielded a counter-model verified by

satisfies_modal().

"unknown" — the search hit the world/step bound, or an open branch’s model

failed verification (so neither verdict is safe to assert).

Mirrors the valid / invalid / unknown contract of the local-Isabelle runner (isabelle_decide_modal()), but runs fully in-process with no external prover.

Parameters:

• formula (Node)

• frame (str)

• max_worlds (int)

• max_steps (int)

Return type:

str