The two research papers: "Quantum Probabilistic Dyadic Second-Order Logic" (2013) and "PLQP & Company: Decidable Logics for Quantum Algorithms (2014), contain a new general proof method to show a decidability result. As such the logic we designed is a decidable logical system for reasoning about quantum systems. It is important to note that this result shows for the first time that quantum logic has a great computational advantage over its classical first- (and higher-) order variants which are known to be undecidable. Decidability is an important feature for a logical system to have, as it opens up the road for implementations in the area of quantum computing where we look for logics that can provide the ultimate basis of our new quantum programming languages. The logical design we provided is endowed with tensor operators to capture properties of composite systems and with probabilistic predication formulas for quantum measurements. We have proven the important decidability result via a translation into the first-order logic of real numbers. This work gives us also a clear indicator of how similar logics can be shown to be decidable by using our general proof method.