%0 Journal Article
%T Formal Verification of Robertson-Type Uncertainty Relation
%A Takaaki Masuhara
%A Toru Kuriyama
%A Masakazu Yoshida
%A Jun Cheng
%J Journal of Quantum Information Science
%P 58-70
%@ 2162-576X
%D 2015
%I Scientific Research Publishing
%R 10.4236/jqis.2015.52008
%X 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 <span lang=\"TR\"><a href=\"file:///C:/Users/scirp/Desktop/%E6%96%B0%E5%BB%BA%20Microsoft%20Word%20%E6%96%87%E6%A1%A3.docx#A\"><span lang=\"EN-US\">Appendix</span></a></span><span lang=\"EN-US\">.</span>
%K Formal Verification
%K Proof Assistant Coq
%K Uncertainty Relation
%U http://www.scirp.org/journal/PaperInformation.aspx?PaperID=57074