unicode_fol_kit.int_valid

unicode_fol_kit.int_valid(formula, max_worlds=3, domain_elements=2, max_steps=300000)

Return True iff no intuitionistic counter-model to formula is found.

Propositional: a genuine decision procedure up to max_worlds worlds (the finite-model property), so True means intuitionistically valid. First-order: a sound but incomplete check — True means “no counter-model within the bounds” (not a proof, since first-order intuitionistic validity is undecidable), while False is always backed by a real counter-model from int_countermodel().

Parameters:

• formula (Node)

• max_worlds (int)

• domain_elements (int)

• max_steps (int)

Return type:

bool