Usefulness

Usefulness

• Contributions to proofs of interesting theorems
• Techniques
  • Watch use as parent in inferences
• Examples
  • In set theory,

    ! [X] : equal(union(X,X),X) 

    is useful, but

    ! [X] : equal(X,X) 

    is redundant, and not often useful.

Implementation

• Fraction of children that are interesting
• Usefulness = NumberOfInterestingChildren / NumberOfChildren
• High usefulness is good