Isabelle/HOL 中的量子投影测量与 CHSH 不等式
计算机科学中的逻辑
2021-03-16 v1
摘要
我们给出了量子投影测量在 Isabelle/HOL 中的形式化，这是一类涉及正交投影算符、在量子计算中频繁使用的测量。我们还形式化了 CHSH 不等式，这是一个在任意概率空间上成立的结论，可用于反驳量子力学存在定域隐变量理论。
引用
@article{arxiv.2103.08535,
title = {Quantum projective measurements and the CHSH inequality in Isabelle/HOL},
author = {Mnacho Echenim and Mehdi Mhalla},
journal= {arXiv preprint arXiv:2103.08535},
year = {2021}
}