Deduction

Technique

• Generate logical consequences by deduction
• Possibly with guidance towards interesting theorems

A Grand Challenge

• The search space is O(N ^2SearchDepth)
• How to focus on "interesting" theorems?
• No goal ... less pruning and ordering
• Need to search more of the space?

Give me your boring,
 your trivial,
 your huddled theorems,
 yearning TPTP