APRILS - Prophesying Axiom Relevance
by Latent Semantic Analysis

Idea

• Used for analysing relationship between documents
• Analogy - Formula = Document; Symbol = Word

Computing LSA Relevance

• Compute initial contextual symbol relationship strengths
• Iterate to take transitivity into account
• Compute formula symbol strength vectors
• LSA relevance between formulae is dot product of their vectors

Evaluation vs. Prophet

• 1337 problems with proofs by EP
• Compare highest ranks of axioms in proof
• APRILS wins 49%, Prophet wins 28%
• APRILS better on larger problems