Summary: 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 ^{ \geq 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.
For the entire collection see [Zbl 1270.03021].