Aims and Motivations

Aims

• To build an ATP system capable of solving
  • More problems
  • Within the same resource limits

Motivation

• Different systems solve different problems at different speeds
  • Deduction techniques used
  • Syntactic characteristics of the problems
• ATP systems quickly solve most problems that they can solve
• Take advantage of individual system strengths