Quantum probabilistic dyadic second-order logic

Alexandru Baltag, Jort M. Bergfeld, Kohei Kishida, Joshua Sack, Sonja J.L. Smets, Shengyang Zhong

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We propose an expressive but decidable logic for reasoning about quantum systems. The logic is endowed with tensor operators to capture properties of composite systems, and with probabilistic predication formulas P ≥ r (s), saying that a quantum system in state s will yield the answer 'yes' (i.e. it will collapse to a state satisfying property P) with a probability at least r whenever a binary measurement of property P is performed. Besides first-order quantifiers ranging over quantum states, we have two second-order quantifiers, one ranging over quantum-testable properties, the other over quantum actions. We use this formalism to express the correctness of some quantum programs. We prove decidability, via translation into the first-order logic of real numbers.

Original languageEnglish (US)
Title of host publicationLogic, Language, Information, and Computation - 20th International Workshop, WoLLIC 2013, Proceedings
Number of pages17
ISBN (Print)9783642399916
StatePublished - Oct 9 2013
Externally publishedYes
Event20th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2013 - Darmstadt, Germany
Duration: Aug 20 2013Aug 23 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8071 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference20th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2013

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Quantum probabilistic dyadic second-order logic'. Together they form a unique fingerprint.

Cite this