unicode_fol_kit.ill_prove

unicode_fol_kit.ill_prove(antecedents, goal, max_depth=None, max_steps=200000)[source]

Search for a cut-free ILL derivation of antecedents ⊢ goal.

Returns an ILLDerivation (which check_ill_proof() re-validates before it is handed back, so a search bug can only lose proofs, never invent them) or None.

What ``None`` means. For a !-free sequent the search is a complete, terminating decision procedure — every rule’s premises are strictly smaller than its conclusion, so with the default max_depth (the sequent’s total node count, which no cut-free derivation’s height can exceed) and no step budget, None proves the sequent underivable. When ! occurs the contraction rule !C grows sequents, so the search is bounded (default depth 2·size + 4 and max_steps expansions) and None means only “no derivation found within the bound”.

max_depth counts rule applications along a branch; pass it explicitly to search deeper !-sequents. max_steps bounds total node expansions and is ignored for !-free sequents (where it could otherwise break completeness).

Parameters:
Return type:

ILLDerivation | None