Automated Theorem Proving

What is it?

• Proving logical consequences ... conclusions that follow inevitably from facts
• At the heart of many important computational tasks, e.g., verification, synthesis

How good is it?

• Capable of solving non-trivial problems
• Not capable of solving all problems within realistic time limits
• Empirical evaluation is inevitable
  • No corpus of real world problems
  • An accepted library of test problems - the TPTP