![[Logo] Mathematics @ Instituto Superior Técnico](/img/DM_Ersatz.svg "Mathematics @ Instituto Superior Técnico")
12/11/2004, 15:00 — 16:00 — Room P4.35, Mathematics Building
Sonja Smets, Free University of Brussels
On Quantum Propositional Dynamic Logics
Together with A. Baltag I have been working on quantum
propositional dynamic logics, i.e. on logical calculi that can
handle “quantum information flow”. First, I will
present the syntax and relational semantics for the Logic of
Quantum Actions (LQA). This logic deals with quantum measurements
and evolutions of one physical system. LQA pushes the work on
quantum modal logic one step further into an action-labeled
version. I will show that LQA yields an obvious candidate for
obtaining a completeness result with respect to the lattice of
closed linear subspaces of a Hilbert space. What is known as
standard quantum logic (SQL), emerges in this framework as the
negation free and measurement-only part of LQA. Second, I will
focus on compound quantum systems and on the Logic of Quantum
Programs (LQP) which in addition to LQA can handle entanglements
[1]. I will focus on the specific features of LQP: the presence of
an entanglement operator, how to capture Bell states and specific
quantum logical gates. Using LQP, a correctness proof for the
quantum teleportation protocol can be given.
[1] A. Baltag and S. Smets: "The Logic of Quantum Programs",
TUCS General Publication No 33, Turku Center for Computer Science,
2004.
