The Nature of ATP

"Possibly the hardest subfield of Computer Science" [Slaney]

• Solutions beyond any complexity bound
• Potentially semi- or undecidable
• Many problems cannot currently be solved within realistic resource limits
• Representative of hard Artificial Intelligence

Slow Progress

• Limited commercial payoff
• Diminishing funding
• Hard to attract students
• Hard to maintain motivation
• Loss of interest and confidence
• Hard to focus on areas of progress → Evaulation is a Key