I am wondering if there is an automated way to determine whether a given set of quantum operations is universal.
More precisely, given a set of 1 and 2 qubit gates, can we write a program to determine whether this constitutes a universal gate set? If so, how might we do this?
EDIT: To clarify I'm interested in both approaches which allow exact replacements (as shown below) and approaches which allow approximating any unitary to some finite precision. Perhaps restricting the problem by not allowing arbitrary rotations in the input gateset could make the problem more tractable I'm not sure.
If I was given a set of quantum gates I would try to use the gates I'm given to implement a well known universal gateset.
Take this artificial example...
\begin{equation} S_0 = \{\text{H}, \text{Rx}(\alpha), \text{CZ}\} \end{equation}
I know I can write any single qubit operation with $\{\text{H}, \text{Rx}(\alpha)\}$ as I can reach any point on the Bloch sphere with 3 parameterised rotations in 2 directions (I can implement $\text{Rz}$ in terms of $\text{H}$ and $\text{Rx}$).
From here it's well known that an arbitrary single qubit rotation along with a $\text{CX}$ gate is sufficient for universality and I can realise a $\text{CX}$ using a $\text{CZ}$ with Hadamards on the target qubit. Therefore the set $S_0$ is a universal gate set.
When I try to think of a way to automate this process of using the provided gates to implement a well known universal gateset I'm not sure where to start. It certainly seems like a hard problem.
