Binary Search

Intuition

• Selection of too many unnecessary axioms results in rich theorem
  but
  Some portion of unnecessary axioms still may be selected
• Every axiom to be used in the proof must be selected
  but
  Some axioms are necessary only in a subset of all possible proofs

Definition

• Sort axioms by relevance
• Divide "somewhere in the middle"
• Form axiom reduced problem with conjecture and better part of axioms
• No solution in time allowed:
  • Relevant axiom is missing: add upper half of lower ranked axioms
  • Too many unnecessary axioms: remove lower half of higher ranked axioms

Shortcomings

• Where to divide the axioms?
• What to do on timeout?
• What if the lowest ranked necessary axiom is ranked very low?