kdrag.tactics.skolem

kdrag.tactics.skolem(pf: Proof) → tuple[list[ExprRef], Proof]

Skolemize an existential quantifier.

>>> x = smt.Int("x")
>>> pf = kd.prove(smt.Exists([x], x > 0))
>>> skolem(pf)
([x!...], |= x!... > 0)