Applicability

Applicability

• Number of objects to which theorem applies
• Techniques
  • Test truth of antecedent in models of the axioms
  • Fraction of HU that variables could represent
• Examples
  • The theorem:

    ! [X] : 
      ( ( iseven(X) 
        & isprime(X) ) 
     => isodd(sumofdivisorsof(X)))

    applies to only X = 2
  • X in the formula:

    ! [X] : natural(X)

    X applies to the entire HU, while in:

    ! [X] (odd(X) | even(X))

    in the worst case X applies to maximally half the HU in both places

Implementation

• Measure predicate constraints on universally quantified variables
  • For only CNF formulae
• Adaptivity (of a universallly quantified variable) = 1 / NumberOfOccurencesOfTheVariable
• Applicability = Sum of adaptivities of variables in the theorem
• High applicability is good