Rewriting with Generalized Nominal Unification

Title:Rewriting with Generalized Nominal Unification

Authors:Yunus David Kerem Kutz and Manfred Schmidt-Schauss

Conference:UNIF 2018

Tags:atom variables, critical pair, expression variable, freshness constraint, generalized nominal unification, Knuth-Bendix criterion, nominal rewriting, nominal unification and rewrite rule

Abstract:

We consider rewriting, critical pairs and confluence tests on rewrite rules using nominal notation. Computing critical pairs is done using nominal unification, and rewriting using nominal matching. The progress is that we permit atom variables in the notation and in the unification algorithm, which generalizes previous approaches using usual nominal unification

Rewriting with Generalized Nominal Unification

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

26

1of26

1

2

3

4