JQIS  Vol.5 No.2 , June 2015
Formal Verification of Robertson-Type Uncertainty Relation
Abstract: Formal verification using interactive theorem provers have been noticed as a method of verification of proofs that are too big for humans to check the validity of them. The purpose of this work is to verify the validity of Robertson-type uncertainty relation toward verifying unconditional security of quantum key distributions. We verify the validity of the relation by using proof assistant Coq and it is turned out that the theorem regarding the relation formally holds. The source code for Coq which represents the validity of the theorem is printed in Appendix.
Cite this paper: Masuhara, T. , Kuriyama, T. , Yoshida, M. and Cheng, J. (2015) Formal Verification of Robertson-Type Uncertainty Relation. Journal of Quantum Information Science, 5, 58-70. doi: 10.4236/jqis.2015.52008.

[1]   Gordon, M.J.C. (1986) Why Higher-Order Logic Is a Good Formalism for Specifying and Verifying Hardware. In: Milne, G.J. and Subrahmanyam, P.A., Eds., Proceedings of the 1985 Edinburgh Workshop on VLSI, North-Holland, 153-177.

[2]   Boyer, R.S., Moore, J.S. and Kaufmann, M. (1996) ACL2 Version 7.0.

[3]   University of Cambridge Computer Laboratory (1989) Isabelle.

[4]   INRIA (1985) The Coq Proof Assistant.

[5]   Heine, M., Sørensen, B. and Urzyczyn, P. (2006) Lectures on the Curry-Howard Isomorphism. Warsaw University, Poland.

[6]   Feit, W. and Thompson, J.G. (1963) Solvability of Groups of Odd Order. Pacific Journal of Mathematics, 13, 775-1029.

[7]   Bender, H. and Glaubernan, G. (1995) Local Analysis for the Odd Order Theorem. Cambridge University Press, Cambridge.

[8]   Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., et al. (2013) A Machine-Checked Proof of the Odd Order Theorem. Lecture Notes in Computer Science, 7998, 163-179.

[9]   Affeldt, R., Hagiwara, M. and Sénizergues, J. (2014) Formalization of Shannon’s Theorems. Journal of Automated Reasoning, 53, 63-103.

[10]   Shannon, C.E. (1948) A mathematical Theory of Communication. Bell System Technical Journal, 27, 379-423.

[11]   Hayashi, M., Ishizaka, S., Kawachi, A., Kimura, G. and Ogawa, T. (2014) Introduction to Quantum Information Science. Springer.

[12]   Robertson, H.P. (1929) The Uncertanty Principle. Physical Review, 34, 163-164.

[13]   Bennett, C.H. and Brassard, G. (1984) Quantum Cryptography: Public Key Distribution and Coin Tossing. Proceedings of IEEE International Conference on Computers Systems and Signal Processing, Bangalore, 175-179.

[14]   Biham, E., Boyer, M., Boykin, P.O., Mor, T. and Roychowdhury, V. (2000) A Proof of the Security of Quantum Key Distribution. Proceedings of 32nd Annual ACM Symposium on the Theory of Computing, New York, 715-724.

[15]   Miyadera, T. and Imai, H. (2006) Information-Disturbance Theorem for Mutually Unbiased Observables. Physical Review A, 73, Article ID: 042317.

[16]   Miyadera, T. and Imai, H. (2007) Information-Disturbance Theorem and Uncertainty Relation.

[17]   Maassen, H. and Uffink, J.B.M. (1988) Generalized Entropic Uncertainty Relations. Physical Review Letters, 60, 1103.

[18]   Krishna, M. and Parthasarathy, K.R. (2002) An Entropic Uncertainty Principle for Quantum Measurements. Sankhya: The Indian Journal of Statistics, Series A, 64, 842-852.