kdrag.utils.bysect

kdrag.utils.bysect(thm, by: list[Proof] | dict[object, Proof], **kwargs) → Sequence[tuple[object, Proof]]

Bisect the by list to find a minimal set of premises that prove thm. Presents the same interface as prove

>>> x,y,z = smt.Ints("x y z")
>>> by = [kd.prove(x + 1 > x), kd.axiom(x == y), kd.prove(y + 1 > y), kd.axiom(y == z)]
>>> bysect(x == z, by=by)
[(1, |= x == y), (3, |= y == z)]

Parameters:

by (list[Proof] | dict[object, Proof])

Return type:

Sequence[tuple[object, Proof]]