kdrag.kernel.prove

kdrag.kernel.prove(thm: BoolRef, by: Proof | Iterable[Proof] = [], admit=False, timeout=1000, dump=False, solver=None) → Proof

Prove a theorem using a list of previously proved lemmas.

In essence prove(Implies(by, thm)).

Parameters:

• thm (smt.BoolRef) – The theorem to prove.

• thm – The theorem to prove.

• by (list[Proof]) – A list of previously proved lemmas.

• admit (bool) – If True, admit the theorem without proof.

Returns:

A proof object of thm

Return type:

Proof

>>> prove(smt.BoolVal(True))
|= True
>>> prove(smt.RealVal(1) >= smt.RealVal(0))
|= 1 >= 0