We introduce two modal natural deduction systems, MSQS and MSpQS, which are suitable to represent and reason about transformations of quantum states in an abstract, qualitative, way. Our systems provide a modal framework for reasoning about operations on quantum states (unitary transformations and measurements) in terms of possible worlds (as abstractions of quantum states) and accessibility relations between these worlds. We give a Kripke–style semantics that formally describes quantum state transformations, and prove the soundness and completeness of our systems with respect to this semantics.We also prove a normalization result for MSQS and MSpQS, showing that all derivations can be reduced to a normal form that satisfies a subformula property and yields a syntactic proof of the consistency of our deduction systems.

Modal Deduction Systems for Quantum State Transformations

MASINI, Andrea;VIGANO', Luca;ZORZI, Margherita
2011

Abstract

We introduce two modal natural deduction systems, MSQS and MSpQS, which are suitable to represent and reason about transformations of quantum states in an abstract, qualitative, way. Our systems provide a modal framework for reasoning about operations on quantum states (unitary transformations and measurements) in terms of possible worlds (as abstractions of quantum states) and accessibility relations between these worlds. We give a Kripke–style semantics that formally describes quantum state transformations, and prove the soundness and completeness of our systems with respect to this semantics.We also prove a normalization result for MSQS and MSpQS, showing that all derivations can be reduced to a normal form that satisfies a subformula property and yields a syntactic proof of the consistency of our deduction systems.
Quantum computing; modal logics; natural deduction; labelled deduction; proof theory
File in questo prodotto:
File Dimensione Formato  
QuantumRegisters-journal.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Dominio pubblico
Dimensione 387.9 kB
Formato Adobe PDF
387.9 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/435082
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 10
social impact