Motivation for Verifying Derivations

ATP systems are complex ... may have bugs

Incompleteness

Failure to complete a derivation
Unavoidable (with finite resources) but tolerable

Unsoundness

Falsely reporting logical consequence
Soundness is typically "mission critical"

Incorrectness

Outputing an incorrect derivation
A correct system is necessarily sound