unicode_fol_kit.lambek_prove¶

unicode_fol_kit.lambek_prove(sequence, goal)[source]¶

Decide sequence ⊢ goal in the Lambek calculus L; return a derivation or None.

This is a genuine decision procedure (see the module docstring): a None proves the sequent underivable in L. The returned derivation is re-validated by check_lambek_proof() before it is handed back, so a search bug can only lose proofs, never invent them.

Raises ValueError on an empty sequence — L requires nonempty antecedents (Lambek’s restriction).

Parameters:

sequence (Iterable[Node])
goal (Node)

Return type:

LambekDerivation | None