unicode_fol_kit.satisfies_modal¶

unicode_fol_kit.satisfies_modal(formula, model, world)[source]¶

Return whether formula is true at world in the Kripke model.

The Kripke satisfaction relation for the propositional / ground modal fragment:

Atom — its Unicode key is in the world’s valuation.
Nominal i — true iff world IS the world model.nominals[i] names (a nominal holds at exactly one world).
At(i, φ) — φ holds at the world named i, regardless of the current world (the hybrid satisfaction operator @i φ).
Not / And / Or / Xor / Implies / Iff — the classical truth tables, recursing at the same world.
Box φ — φ holds at every "alethic"-successor; Diamond φ — at some "alethic"-successor.
Knows(a, φ) — φ holds at every "K:"+a-successor (universal).
Believes(a, φ) — φ holds at every "B:"+a-successor (universal).
Obligatory φ — φ holds at every "deontic"-successor (universal); Permitted φ — at some "deontic"-successor.
Next φ — φ holds at every immediate "temporal"-successor.
Always φ / Eventually φ — φ holds at all / some worlds in the reflexive-transitive closure of "temporal" from world.
Until(φ, ψ) — see _until_holds() (finite-path strong Until).

Raises:

NotImplementedError – on a Quantifier / SortedQuantifier (first-order modal logic is out of scope for v1), a Łukasiewicz node, or a lambda node.

Parameters:

Return type:

bool