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 A.; VIGANO' L.; ZORZI M.. - In: JOURNAL OF MULTIPLE VALUED LOGIC & SOFT COMPUTING. - ISSN 1542-3980. - STAMPA. - 17:5-6(2011), pp. 475-519.
Titolo: | Modal Deduction Systems for Quantum State Transformations |
Autori: | |
Data di pubblicazione: | 2011 |
Rivista: | |
Citazione: | Modal Deduction Systems for Quantum State Transformations / MASINI A.; VIGANO' L.; ZORZI M.. - In: JOURNAL OF MULTIPLE VALUED LOGIC & SOFT COMPUTING. - ISSN 1542-3980. - STAMPA. - 17:5-6(2011), pp. 475-519. |
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. |
Handle: | http://hdl.handle.net/11562/435082 |
Appare nelle tipologie: | 01.01 Articolo in Rivista |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
QuantumRegisters-journal.pdf | Documento in Post-print | ![]() | Administrator Richiedi una copia |