unicode_fol_kit.prove_tableau

unicode_fol_kit.prove_tableau(premises, conclusion, max_steps=20000, max_terms=8)

Return True iff premises entail conclusion (premises + ¬conclusion close).

For modal inputs this is local consequence over the system K (see unicode_fol_kit.atp.modal_tableau.modal_prove() for other frames).

Parameters:

• conclusion (Node)

• max_steps (int)

• max_terms (int)

Return type:

bool