A Qualitative Modal Representation of Quantum Register Transformations

We introduce two modal natural deduction systems that are suitable to represent and reason about transformations 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 operations. Our systems provide a modal framework for reasoning about operations on quantum registers (unitary transformations and measurements), in terms of possible worlds (as abstractions of quantum registers) and accessibility relations between these worlds. We give a Kripke--style semantics that formally describes quantum register transformations and prove the soundness and completeness of our systems with respect to this semantics.