unicode_fol_kit.find_fitch_proof¶

unicode_fol_kit.find_fitch_proof(premises, conclusion, max_depth=8)[source]¶

Search for a Fitch proof of premises ⊢ conclusion; return it or None.

Goal-directed backtracking over the classical propositional + first-order rules. The returned proof is re-validated by check_proof before it is handed back, so the result is always a genuinely valid proof (or None). None means “no proof found within max_depth”, never “not a theorem” — the search is sound but, under its depth bound, incomplete (first-order provability is undecidable).

Parameters:

conclusion (Node)
max_depth (int)

Return type:

Proof | None