unicode_fol_kit.tableau_model

unicode_fol_kit.tableau_model(formulas, max_steps=20000, max_terms=8)

Return a satisfying literal assignment if formulas are satisfiable, else None.

On an open (saturated) branch the literals are returned as a dict mapping each atom’s surface form to its truth value; None means the tableau closed (unsatisfiable) within the bound.

A modal model is a Kripke structure, not a flat literal assignment, so a modal input is rejected here with a pointer to unicode_fol_kit.atp.modal_tableau.modal_countermodel(), which returns a verified KripkeModel.

Parameters:

• max_steps (int)

• max_terms (int)

Return type:

dict | None