Binary Search

Algorithm

• Provide axioms with relevance measure
• Divide formulae into top and bottom parts
• Call ATP system using the top part
  • If proof found, hoorah
  • If proof impossible, add top of bottom
  • If timeout
    • Optimistic mode, try top of top
    • Pessimistic mode, add top of bottom

Dividing Strategies

• At the median - get half the formulae
• At 0.5 - get formulae "more than half relevant"
• At the (geometric) average - get formulae "above average relevance"
• Σtop-relevancies = Σbottom-relevancies - get "half the relevance"
• Σtop-relevancies = Σ(1 - bottom-relevancies) - balances relevance against irrelevance
• Σ(1 - top-relevance) = Σbottom-relevancies - balances irrelevance against relevance.