Aims and Motivations

Automated Theorem Proving (ATP)

• Proving logical consequences ... conclusions that follow inevitably from facts
• At the heart of many important computational tasks
• Capable of solving non-trivial problems
• Not capable of solving all problems
  • The Peter Principle Point
  • Can be tuned to solve some problems
  • But then cannot solve solve some other problems

Aims

• Breadth of coverage - solve all problems any system can solve
• Depth of coverage - solve problems that no system can solve