Measuring Relevance

Background

• A relevance measure measures relevance of a formula to a conjecture
• Necessarily approximate (or P = NP)
• Adopt ideas from document retrieval research
• Variations galore

• The contextual intersection Π between Fa and Fc in the context of the set S is

                             |{f:f∈S,s∈sym(f)}|
  ∑                    ( 1 - ------------------- )
  s∈(sym(Fa)∩sym(Fb))               |S| 

• The contextual direct relevance between Fa and Fc in the context of the set S is

  |sym(Fa) Π sym(Fc)|
  --------------------
  |sym(Fa) ∪ sym(Fc)| 

• The "weakest link" path relevance between Fa and Fc is

  min      direct-relevance(Fi-1,Fi)
  i=1..n
  ----------------------------------
                  n    

• The transitive relevance between Fa and Fc is

  max path-relevance(Fa,Fc)