Tags:Axiom selection, First order theorem proving, Large knowledge base, Natural language commonsense problems, SUMO and Word embedding

Abstract:

First order theorem proving with large knowledge bases makes it necessary to select those parts of the knowledge base, which are necessary to prove the theorem at hand. We propose to extend syntactic axiom selection procedures like SInE to the use of the semantics of symbol names. For this not only occurrences of symbol names but also similar names are taken into account. We propose to use a similarity measure based on word embeddings like ConceptNet Numberbatch. An evaluation of this similarity based SInE is given by using problem sets from TPTP's CSR problem class and Adimen-SUMO. This evaluation is done with two very different systems, namely the HYPER tableau prover and the saturation based system E.

Names are not just Sound and Smoke: Word Embeddings for Axiom Selection