论文标题
自然扣除的新连接及其在量子计算中的应用
A New Connective in Natural Deduction, and its Application to Quantum Computing
论文作者
论文摘要
我们研究了逻辑上的连接器与无与伦比的扣除规则（例如Prior's Tonk和Quantum Computing）之间的无引起的联系。我们认为，这些缔合模型在量子测量中进行了信息搜索，非可逆性和非确定性。我们引入了一种直觉的命题逻辑，该命题逻辑具有无与伦比的逻辑结缔组织和两个间隙规则，并证明了该逻辑的证明语言构成了量子编程语言的核心。
We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue that these connectives model the information-erasure, the non-reversibility, and the non-determinism that occur, among other places, in quantum measurement. We introduce an intuitionistic propositional logic with a non-harmonious logical connective sup and two interstitial rules, and show that the proof language of this logic forms the core of a quantum programming language.
