Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection
Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection
复制标题
DOI：
10.1007/978-3-030-29436-6_15
复制
发表时间：
2019-08
期刊：
影响因子：
--
通讯作者：
U. Furbach;Teresa Krämer;C. Schon
中科院分区：
文献类型：
--
作者：
U. Furbach;Teresa Krämer;C. Schon
具有大型知识库的一阶定理证明使得有必要选择知识库中证明手头定理所必需的那些部分。我们扩展语法公理选择过程，如SInE使用符号名称的语义。为此，不仅要考虑符号名称的出现，还要考虑语义相似的名称。我们使用基于词嵌入的相似性度量。这种相似性的基础上SInE的评价给出使用TPTP的CSR问题类和Adimen-SUMO的问题。这个评估是用两个非常不同的系统完成的，即Hyper tableau prover和基于饱和度的系统E。
First-order theorem proving with large knowledge bases makes it necessary to select those parts of the knowledge base, that are necessary to prove the theorem at hand. We extend syntactic axiom selection procedures like SInE to use semantics of symbol names. For this, not only occurrences of symbol names but also semantically similar names are taken into account. We use a similarity measure based on word embeddings. An evaluation of this similarity based SInE is given using problems 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.