unicode_fol_kit.prove

unicode_fol_kit.prove(premises, conclusion, max_steps=10000)

Return True iff premises entail conclusion (premises ⊨ conclusion).

Decided by refutation. Each premise is treated as a sentence: free variables are read as universally quantified (its universal closure). The conclusion is universally closed and then negated — crucially in that order, because ¬∀x φ is ∃x ¬φ: a free variable of the conclusion must skolemise to a fresh witness constant/function under the negation, NOT to a universally quantified variable. (Closing after negating would misplace the ∀ outside the ¬ and unsoundly turn ∃x ¬φ into ∀x ¬φ.) Each source formula is clausified independently and every clause is renamed apart, so the Skolem and variable names from one source cannot collide with another’s. The clause sets are unioned and saturation is run. Returns True iff the empty clause is derived; False if the union saturates without it; and False (conservatively, “not proved within the bound”) if max_steps is reached first — never reporting a non-theorem as proved.

Parameters:

• conclusion (Node)

• max_steps (int)

Return type:

bool