Abstract. A new logic is proposed for reasoning about quantum systems. The logic embodies the postulates of quantum physics and it was designed from the semantics upwards by identifying quantum models with superpositions of classical models. This novel approach to quantum logic is completely different from the traditional approach of Birkhoff and von Neumann. It has the advantage of making quantum logic an extension of classical logic. The key new ingredient of the language of the proposed logic is a rather general modal operator. The logic incorporates probabilistic reasoning (in the style of Nilsson) in order to deal with uncertainty on the outcome of measurements. The logic also incorporates dynamic reasoning (in the style of Hoare) in order to cope with the evolution of quantum systems. A Hilbert calculus for the logic is sketched. A quantum key distribution protocol is specified and analyzed. 1 Motivation and Related Work A new logic is proposed for modeling and reasoning about...