Efficient encodings of first-order Horn formulas in equational logic

Title:Efficient encodings of first-order Horn formulas in equational logic

Authors:Nicholas Smallbone and Koen Claessen

Conference:IJCAR-2018

Tags:automated theorem proving, equational logic, first-order logic, horn clause and unit equality

Abstract:

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 the translations we were able to solve 33 problems of rating 1.0 from the TPTP.