Background

Definition

• A relevance measure measures relevance of a formula to a conjecture
• Necessarily approximate (or P = NP)
• Used to include/exclude formulae from a proof attempt
• Related to quality measures which order formulae for use as parents

Previous Work

• Common syntactic CNF quality measures
• System specific FOF quality measures
• Plaisted & Yayha, Veroff's relevance measures use possibility of inference from formula abstractions
• RedAx relevance measure used formula weight

Principle of "Aboutness"

• Is the formula "talking about the same things" as the conjecture?
• Measure extent to which they share predicates and functors
• Also used for partition-based reasoning