Efficient encodings of first-order Horn formulas in equational logic
Authors: Nicholas Smallbone and Koen Claessen
Paper Information
| Title: | Efficient encodings of first-order Horn formulas in equational logic |
| Authors: | Nicholas Smallbone and Koen Claessen |
| Proceedings: | IJCAR Proceedings 9th IJCAR, 2018 |
| Editors: | Stephan Schulz, Didier Galmiche and Roberto Sebastiani |
| Keywords: | first-order logic, equational logic, unit equality, automated theorem proving |
| Abstract: | 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. |
| Pages: | 16 |
| Talk: | Jul 16 12:00 (Session 111E: Superposition) |
| Paper: |  |