kdrag.theories.sexp.Truth
- kdrag.theories.sexp.Truth(pf: Proof) tuple[ExprRef, Proof, Proof, Proof]
https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem
>>> p = kd.prove(smt.BoolVal(True)) >>> Truth(p) (Sexp("(declare-fun F (Bool) Bool) (assert (F true)) "), |= truth(Sexp("(declare-fun F (Bool) Bool) (assert (F true)) ")), |= has_interp(Sexp("(declare-fun F (Bool) Bool) (assert (F true)) "), True), |= interp(Sexp("(declare-fun F (Bool) Bool) (assert (F true)) ")) == True)