kdrag.kernel.herb

kdrag.kernel.herb(thm: QuantifierRef, prefixes=None) → tuple[list[ExprRef], Proof]

Herbrandize a theorem. It is sufficient to prove a theorem for fresh consts to prove a universal. Note: Perhaps lambdaized form is better? Return vars and lamda that could receive |= P[vars]

>>> x = smt.Int("x")
>>> herb(smt.ForAll([x], x >= x))
([x!...], |=  Implies(x!... >= x!..., ForAll(x, x >= x)))

Parameters:

thm (QuantifierRef)

Return type:

tuple[list[ExprRef], Proof]