unicode_fol_kit.modal_prove

unicode_fol_kit.modal_prove(premises, conclusion, frame='K', systems=None, max_worlds=400, max_steps=200000)

Return True iff premises locally entail conclusion over frame.

Local consequence: the tableau for premises ∪ {¬conclusion} at one world closes. Sound (a True is a closed tableau); incomplete only up to the bound.

Parameters:

• conclusion (Node)

• frame (str)

• max_worlds (int)

• max_steps (int)

Return type:

bool