What has Operational Quantum Logic to do with Linear Logic

Leopoldo Rom�n

Akira Oide

Tsubasa Takagi

Although various dynamic or temporal logics have been proposed to verify quantum protocols and systems, these two viewpoints have not been studied comprehensively enough. We propose Linear Temporal Quantum Logic (LTQL), a linear temporal extension of quantum logic with a quantum implication, and extend it to Dynamic Linear Temporal Quantum Logic (DLTQL). This logic has temporal operators to express transitions by unitary operators (quantum gates) and dynamic ones to express those by projections (projective measurement). We then prove some logical properties of the relationship between these two transitions expressed by LTQL and DLTQL. A drawback in applying LTQL to the verification of quantum protocols is that these logics cannot express the future operator in linear temporal logic. We propose a way to mitigate this drawback by using a translation from (D)LTQL to Linear Temporal Modal Logic (LTML) and a simulation. This translation reduces the satisfiability problem of (D)LTQL formulas to that of LTML with the classical semantics over quantum states.

Ma Lei

In this paper, by using the linear quantum transformation theory to spin operator, we offer an effective method to study the quantum logic gates based on spin - 1/2 states. The forms of some basic quantum logic operations are also obtained.

J. D. Franson, B. C. Jacobs, T. B. Pittman

Abstract Probabilistic quantum logic operations can be implemented using linear optical elements, additional photons (ancilla), and post‐selection based on the results of measurements made on the ancilla photons. Here we describe the experimental demonstration of several quantum logic devices of that kind, including a quantum parity check and a destructive controlled‐NOT (CNOT) gate. An experimental demonstration of feed‐forward control for use in quantum logic operations is also reported. The implementation of a conventional CNOT gate using polarizing beam splitters is described, along with a new “high‐fidelity” approach in which the logic gates always produce an output.

Bob Coecke, David Moore, Alexander Wilce