Generating Theorems

Generating Theorems

• Traditional ATP ignores as much of the space as possible
• Are there other unnoticed interesting theorems in the space?
• People think so
  • Newell and Simon's prediction
  • Alan Bindy's DReaM
  • Bob Kowalski's opinion
• Systems' have (helped) to find some
  • AM's conjectures
  • Otter and EQP proofs of open and new conjectures
  • McCune's new axiomatizations of theories
  • Chu's investigations in plane geometry
  • HR's conjectures

Approaches

• Typical use is to generate conjectures and test with ATP
  • Induction
  • Construction
  • Manipulation
• AGInT approach is to generate logical consequences and extract theorems
  • Deduction
  • Also now used by Roy MacHasland
  • ATP becomes part of the problem, not the solution