unicode_fol_kit.is_valid_resolution

unicode_fol_kit.is_valid_resolution(formula, max_steps=10000)[source]

Return True iff formula is valid (its negation is refutable).

Equivalent to prove([], formula): a formula is valid exactly when ¬formula is unsatisfiable, which resolution decides by deriving the empty clause from the clauses of ¬formula. Incomplete under the bound: a return of False means “not shown valid within max_steps”, never a false claim of invalidity-as-validity.

Parameters:
Return type:

bool