  Selection strategies are broadly used in first-order logic theorem proving to
select those parts of a large knowledge base that are necessary to proof a
theorem at hand. Usually, these selection strategies do not take the meaning of
symbol names into account. In knowledge bases with commonsense knowledge,
symbol names are usually chosen to have a meaning and this meaning provides
valuable information for selection strategies. We introduce the vector-based
selection strategy, a purely statistical selection technique for commonsense
knowledge based on word embeddings. We compare different commonsense knowledge
selection techniques for the purpose of theorem proving and demonstrate the
usefulness of vector-based selection with a case study.
