Reasoning foundations
Soundness
The property that accepted results are valid under the stated semantics.
Definition
Soundness
A reasoning procedure is sound if every result it accepts follows from its rules and assumptions.
Soundness does not require the procedure to solve every valid input. A sound but incomplete procedure can return unknown when it lacks a supported route.
01
Example
A proof kernel is sound for its calculus if every accepted proof term has the type the kernel reports.
02
Important distinction
Passing a large test suite is evidence about an implementation, not a proof of soundness by itself.
After reading this article, you should be able to
- Define Soundness in the sense used on this site.
- Distinguish soundness from completeness and benchmark coverage.