Obviousness

Obviousness

• LCs reasonably difficult to prove
• Techniques
  • Size of proof tree
  • Time for proof
• Examples
  • The proof of the critical Robbins problem lemma is long
  • Otter finds a short proof of reflexivity from set axioms

Implementation

• Limit proof tree size
• Axioms have proof tree size 0
• LCs have proof tree size = sum of parents sizes plus 1
• High proof tree size is good