  We introduce a class of rooted graphs which allows one to encode various
kinds of classical or quantum circuits. We then follow a set-theoretic approach
to define rewrite systems over the considered graphs and propose a new complete
Superposition callculus which handles sets of formulas consisting of equations
or disequations over these graphs.
