Efficient algorithms for computing modulo permutation theories

Abstract

In automated deduction it is sometimes helpful to compute modulo a set E of equations. In this paper we consider the case where E consists of permutation equations only. Here a permutation equation has the form f(x1,..., xn) = f(xπ(1),...,xπ(n)) where π is a permutation on {1,..., n}. If E is allowed to be part of the input then even testing E-equality is at least as hard as testing for graph isomorphism. For a fixed set E we present a polynomial time algorithm for testing E-equality. Testing matchability and unifiability is NP-complete. We present relatively efficient algorithms for these problems. These algorithms are based on knowledge from group theory.