unicode_fol_kit.so_is_valid_finite

unicode_fol_kit.so_is_valid_finite(formula, max_size=3, max_candidates=4194304)

True iff no finite counter-model of the SO formula is found up to max_size.

Bounded and one-sided: True is strong evidence of second-order validity (not a proof — SO validity is not semi-decidable); False is a genuine refutation, with the witness available from so_find_countermodel().

Parameters:

• formula (Node)

• max_size (int)

• max_candidates (int)

Return type:

bool