| ||||
| ||||
![]() Title:Efficient encodings of first-order Horn formulas in equational logic 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. Efficient encodings of first-order Horn formulas in equational logic ![]() Efficient encodings of first-order Horn formulas in equational logic | ||||
Copyright © 2002 – 2025 EasyChair |