Quantum logic and linear logic

Akira Oide

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

Peter Mittelstaedt

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.

Vaughan Pratt

Quantum logic is static, describing automata having uncertain states but no state transitions and no Heisenberg uncertainty tradeoff. We cast Girard's linear logic in the role of a dynamic quantum logic, regarded as an extension of quantum logic with time nonstandardly interpreted over a domain of linear automata and their dual linear schedules. In this extension the uncertainty tradeoff emerges via the "structure veil." When VLSI shrinks to where quantum effects are felt, their computer-aided design systems may benefit from such logics of computational behavior having a strong connection to quantum mechanics. 1 Motivation VLSI designers will eventually need to reckon with quantum mechanics (QM), certainly within 50 years and possibly by the 2010's. Computer-aided design (CAD) tools will need to adapt accordingly. Does this entail changing only the theory or also the logic of CAD verification systems? That is, will it be enough just to change those nonlogical axioms defining how elect...

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.