A Qualitative Modal Representation of Quantum Register Transformations

TL;DR

This paper introduces two modal natural deduction systems that provide an abstract, qualitative framework for reasoning about transformations of quantum registers, capturing quantum operations as possible worlds and accessibility relations.

Contribution

It presents novel modal logic systems with formal semantics for representing and reasoning about quantum register transformations, bridging quantum computing and modal logic.

Findings

Soundness and completeness of the systems are proven.

The framework models quantum operations as modal accessibility relations.

Provides a formal semantic foundation for quantum register transformations.

Abstract

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.