Motivation, History, and Overview

Large Theories

• Many functors and predicates, many (common) axioms, many theorems
• SUMO, Cyc, Mizar, YAGO, WordNet, MeSH
• Different challenges for ATP
  • Parsing and building data structures
  • Loading and preprocessing the common axioms only once
  • Selecting axioms that are likely to be useful
  • Extracting heuristics and lemmas from proofs

Selecting Axioms that are Likely to be Useful

• To obtain a proof of a given conjecture
• Select just enough axioms to obtain a proof
• Previous work

This Work

• Two syntactic relevance orderings
• (More) robust selection that "starts in the middle"
• Evaluation shows it's effective