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.

Efficient encodings of first-order Horn formulas in equational logic

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

1of25

1

2

3

4