Efficient Encodings of First-Order Horn Formulas in Equational Logic.
Lecture Notes in Artificial Intelligence(2018)
摘要
We present several translations from first-order Horn formulas to equational logic. The goal of these translations is to allow equational theorem provers to efficiently reason about non-equational problems. Using these translations we were able to solve 37 problems of rating 1.0 (i. e. which had not previously been automatically solved) from the TPTP.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络