unicode_fol_kit.rel_satisfies

unicode_fol_kit.rel_satisfies(model, world, formula)

Return whether formula is true at world in model.

Implements the simplified Routley–Meyer clauses: atoms via the valuation, ∧/∨ pointwise, ¬A true at w iff A is false at w*, A → B at a normal world iff every world satisfying A satisfies B, and at a non-normal world iff x ⊨ A ⇒ y ⊨ B for every triple R(w, x, y). A ↔ B unfolds to (A → B) ∧ (B → A).

Raises TypeError for non-propositional input (quantifiers, modalities, lambdas, non-nullary atoms) and ValueError for an unknown world.

Parameters:

• model (RelevantModel)

• world (str)

• formula (Node)

Return type:

bool