Soundness and Completeness

Soundness

• Sound systems return only correct solutions
  • Unsound systems are useless

• Soundness required

Completeness

• Complete systems always return a solution if one exists

• Issues that affect (practical) completeness
  • Theory (calculus, search control)
  • Implementation (speed, bugs!)
  • Resource limits (hardware, CPU time limit)

• For a user, all forms of incompleteness are the same
• Supply of resources is not under an ATP system's control

• Theoretical and practical completeness not required