kdrag.kernel.modus

kdrag.kernel.modus(ab: Proof, a: Proof) → Proof

Modus ponens

>>> a,b = smt.Bools("a b")
>>> ab = axiom(smt.Implies(a, b))
>>> a = axiom(a)
>>> modus(ab, a)
|- b

Parameters:

• ab (Proof)

• a (Proof)

Return type:

Proof