unicode_fol_kit.fuzzy_is_valid

unicode_fol_kit.fuzzy_is_valid(formula, timeout=10000, tnorm='lukasiewicz', domain=None, sort_universes=None)

Return True iff the formula has degree 1 under every atom-valuation.

Checks validity by asserting degree < 1 together with the [0, 1] atom bounds: if that is unsatisfiable, no valuation drops the degree below 1, so the formula is valid. A Z3 unknown result returns False.

tnorm selects the strong-connective semantics ("lukasiewicz" / "godel"); a quantified formula is grounded over domain / sort_universes first.

Parameters:

• formula (Node)

• timeout (int)

• tnorm (str)

Return type:

bool