Deduction

Technique

• Select consistent axioms
• Deduce logical consequences (modulo subsumption?)
• Identify the theorems, i.e., the interesting ones
• Possibly with guidance towards interesting theorems

Advantages

• Produces only theorems
• Impossible for ponderous humans ...
  Hope for new interesting theorems

Disadvantages

• Generates very very many boring theorems
• Requires guidance or filtering