unicode_fol_kit.is_valid_finite

unicode_fol_kit.is_valid_finite(formula, max_size=4, max_candidates=1048576)

True iff no finite countermodel of formula exists up to max_size (bounded).

Bounded and one-sided: True means “no countermodel found within the bounds” (strong evidence of validity, not a proof); a False is a genuine refutation — find_countermodel() returns the witnessing structure.

Parameters:

• formula (Node)

• max_size (int)

• max_candidates (int)

Return type:

bool