A Qualitative Modal Representation of Quantum Register Transformations

We introduce two modal natural deduction systems that are suitable to represent and reason about transforma- tions of quantum registers in an abstract, qualitative, way. Quantum registers represent quantum systems, and can be viewed as the structure of quantum data for quantum oper- ations. Our systems provide a modal framework for reason- ing about operations on quantum registers (unitary trans- formations and measurements) in terms of possible worlds (as abstractions of quantum registers) and accessibility re- lations between these worlds. We give a Kripke–style se- mantics that formally describes quantum register transfor- mations, and prove the soundness and completeness of our systems with respect to this semantics.