Soundness

Definition. A proof theory is sound if whenever $P_1,P_2,\dots ,P_n⊢Q$ (proof) then $P_1,P_2,\dots ,P_n\models Q$ (truth/valid).

Reminder from Logic: $|-$ → Proof Theory, pronounced “proves” $\models$ → Semantics, pronounced “entails” / “valid” / “semantic entailment”

Algorithm

From F1TENTH.

An algorithm is said to be complete if

• if terminates in finite time and
• it returns a solution when one exists and it returns failure otherwise

Oh, this sounds awfully like Total Correctness in SE212.

Related

• Completeness