A classical proof system for quantum unsatisfiability, based on a matrix Nullstellensatz

We define the first nontrivial proof system for the complement of quantum satisfiability ( ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ 𝖰 𝖲 𝖠 𝖳 ). The system uses left-ideal rules in the ring of linear operators on an n -qubit register. Implicational completeness is given by a matricial version of Hilbert's Nullstellensatz. We prove two distinct forms of the system to be equivalent respectively to Resolution and Polynomial Calculus with Resolution in the classical subcase. The systems are efficiently verifiable by a classical TM. We also discuss the matter of quantum proof systems for ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ ̅ 𝖰 𝖲 𝖠 𝖳 .