On the complexity of theories of permutations
The first-order theory T of two permutations which commute is investigated and its decidability is proved. Moreover, we show that the computational complexity of the decision algorithm for SAT(T) - on NTM's and ATM's - is the same (for upper and lower bounds) as that of the theory of one permutation.
scientific article; zbMATH DE number 3991472