Logical Consequences and Theorems

What is a "Theorem"?

• Axioms have logical consequences (LCs)
• Humans designate interesting LCs as theorems
  In this work "theorem" means "interesting logical consequence"
• Some LCs are designated as lemmas
  In this work lemmas are considered to be a diminutive type of theorem
• Conjectures are unproved theorems

Traditional ATP

• Humans identify conjectures and theorems
• ATP systems search for proofs
  • Refutation style
  • Hilbert style
  by searching for a point (or a few) in the search space
• The search space is O(N ^2SearchDepth)