自然演绎中的一个新连接词及其在量子计算中的应用
A New Connective in Natural Deduction, and its Application to Quantum Computing
AI总结：
本文研究了非和谐逻辑连接词与量子计算的联系，指出其能建模量子测量中的信息擦除等现象，并引入包含sup连接词的直觉主义逻辑，证明其证明语言可作为量子编程语言的核心。
摘要：
我们研究了具有非和谐演绎规则的逻辑连接词（如Prior的tonk）与量子计算之间意想不到的联系。我们认为这些连接词对量子测量等场景中出现的信息擦除、不可逆性和非确定性进行了建模。我们引入了一种带有非和谐逻辑连接词sup和两条间隙规则的直觉主义命题逻辑，并证明该逻辑的证明语言构成了量子编程语言的核心。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
