unicode_fol_kit.rel_valid

unicode_fol_kit.rel_valid(formula, max_worlds=2)[source]

Return True iff no B-countermodel to formula is found within the bound.

HONEST CONTRACT (mirroring int_valid()’s first-order contract): False is definitive — it is backed by an explicit, rel_satisfies()-verified countermodel from rel_countermodel(), so the formula is certainly not a theorem of B. True means only “no countermodel with at most max_worlds worlds”: B is decidable, but this search is bounded, so a non-theorem whose smallest refuting interpretation needs more worlds than the bound is (spuriously) reported valid. Raising max_worlds never turns a False into a True; it is exponentially more expensive (see rel_countermodel()).

Parameters:
Return type:

bool