From basic logic to quantum logic with cut-elimination
From basic logic to quantum logic with cut-elimination
复制标题
DOI：
10.1023/a:1026652903971
复制
发表时间：
1998-01-01
影响因子：
1.4
通讯作者：
Sambin, G
中科院分区：
文献类型：
--
作者：
Faggian, C;Sambin, G
本文介绍的结果是在基本逻辑框架中获得的，这是一种旨在统一多个逻辑系统的新逻辑。第一个结果是序列化的序列公式，该公式允许使用量子逻辑中的证明理论方法。这样的公式承认了一个非常简单的切割淘汰程序，因此，由于属性属性，也是一种证明搜索方法和有效的决策程序。通过使用基本逻辑的框架，我们还获得了与线性正交学的含义的无剪裁配方，并且通常用于广泛的新型量子样逻辑。这些逻辑符合物理学家和计算机科学家表达的一些要求。特别是，我们提出了一个有意义的线性量子逻辑的好候选者。
The results presented in this paper were obtained in the framework of basic logic, a new logic aiming at the unification of several logical systems. The first result is a sequent formulation for orthologic which allows the use of methods of proof theory in quantum logic. Such a formulation admits a very simple procedure of cut-elimination and hence, because of the subformula property, also a method of proof search and an effective decision procedure. By using the framework of basic logic, we also obtain a cut-free formulation for orthologic with implication, for linear orthologic, and, more in generally for a wide range of new quantum-like logics. These logics meet some requirements expressed by physicists and computer scientists. In particular, we propose a good candidate for a linear quantum logic with implication.