unicode_fol_kit.find_countermodel

unicode_fol_kit.find_countermodel(premises, conclusion, max_size=4, max_candidates=1048576)

Return a finite structure satisfying premises but not conclusion, or None.

A countermodel witnesses that premises do not entail conclusion. The conclusion is universally closed and negated, so the structure refutes the entailment for some assignment of its free variables.

Parameters:

• conclusion (Node)

• max_size (int)

• max_candidates (int)

Return type:

Structure | None