unicode_fol_kit.ill_derivable

unicode_fol_kit.ill_derivable(antecedents, goal, max_depth=None, max_steps=200000)

Return True iff ill_prove() finds a derivation of antecedents ⊢ goal.

Decides derivability for !-free sequents; for sequents containing ! a False means only “no derivation within the bound” (see ill_prove()).

Parameters:

• antecedents (Iterable[Node])

• goal (Node)

• max_depth (int | None)

• max_steps (int)

Return type:

bool