unicode_fol_kit.modal_countermodel

unicode_fol_kit.modal_countermodel(formula, frame='K', systems=None, max_worlds=400, max_steps=200000)

Return a Kripke model falsifying formula over frame, or None.

None means the formula is valid (the tableau closed) or the search was inconclusive within the bound. The returned model is verified: it is only handed back when satisfies_modal() confirms the formula is false at its root world, so a counter-model is never spurious.

Parameters:

• formula (Node)

• frame (str)

• max_worlds (int)

• max_steps (int)