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 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.
Cite
CITATION STYLE
Claessen, K., & Smallbone, N. (2018). Efficient Encodings of First-Order Horn Formulas in Equational Logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 388–404). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
