Dynamic Ideas in Quantum Logic

María Luisa Dalla Chiara, Roberto Giuntini

Alexandru Baltag, Sonja Smets

In this paper we show how ideas coming from two areas of research in logic can reinforce each other. The first such line of inquiry concerns the “dynamic turn” in logic and especially the formalisms inspired by Propositional Dynamic Logic (PDL); while the second line concerns research into the logical foundations of Quantum Physics, and in particular the area known as Operational Quantum Logic, as developed by Jauch and Piron (Helve Phys Acta 42:842–848, 1969 ), Piron (Foundations of Quantum Physics, 1976 ). By bringing these areas together we explain the basic ingredients of Dynamic Quantum Logic, a new direction of research in the logical foundations of physics.

Dov M. Gabbay, Kurt Engesser, Daniel J. Lehmann

Jincheng Zhang

This paper presents a novel approach to optimizing quantum logic circuits through adaptive optimization. The core idea centers around dynamically adjusting circuit parameters based on real-time performance evaluation, leveraging reinforcement learning. A "Quantum Logic Optimizer" is constructed, employing reinforcement learning to assess circuit performance and, crucially, integrating quantum error correction and decoherence mitigation techniques to enable dynamic parameter adjustments. The aim is to enhance circuit efficiency and fidelity. The proposed methodology offers a promising path towards improving the performance of quantum logic circuits, particularly in scenarios where the initial circuit design may not be optimal for all possible inputs or operating conditions. This work explores the potential of combining dynamic optimization with established quantum error mitigation strategies, representing a significant step forward in the field.

John Bell

Alexandru Baltag, Sonja Smets

The main contribution of this paper is the introduction of a dynamic logic formalism for reasoning about information flow in composite quantum systems. This builds on our previous work on a complete quantum dynamic logic for single systems. Here we extend that work to a sound (but not necessarily complete) logic for composite systems, which brings together ideas from the quantum logic tradition with concepts from (dynamic) modal logic and from quantum computation. This Logic of Quantum Programs (LQP) is capable of expressing important features of quantum measurements and unitary evolutions of multi-partite states, as well as giving logical characterisations to various forms of entanglement (for example, the Bell states, the GHZ states etc.). We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness proofs for the Teleportation protocol and for a standard Quantum Secret Sharing protocol; a whole range of other quantum circuits and programs, including other well-known protocols (for example, superdense coding, entanglement swapping, logic-gate teleportation etc.), can be similarly verified using our logic.