We review four areas of theoretical computer science which share technical or philosophical ideas with the work of Belnap on his useful four-valued logic. Perhaps surprisingly, the inspiration by Belnap-Dunn logic is acknowledged only in the study of d-frames. The connections of Belnap's work and linear logic, Blame Calculus or the study of LVars are not openly admitted. The key to three of these connections with Belnap's work go via the twist-product representation of bilattices. On the one hand, it allows us to view a large class of models of linear logic as based on Belnap-Dunn logic. On the other hand, d-frames admit two twist-product representation theorems and, also, the key theorem of Blame Calculus is essentially a twist-product representation theorem too, albeit with a strong proof-theoretic flavour.
翻译:本文回顾了理论计算机科学中与Belnap实用四值逻辑工作共享技术或哲学思想的四个领域。或许令人惊讶的是,Belnap-Dunn逻辑的启发仅在d-框架研究中得到明确承认。Belnap工作与线性逻辑、追责演算或LVars研究之间的关联并未被公开确认。其中三个领域与Belnap工作的连接关键,在于双格结构的扭积表示。一方面,这使得我们可以将线性逻辑的广泛模型类视为基于Belnap-Dunn逻辑。另一方面,d-框架允许两种扭积表示定理,同时追责演算的核心定理本质上也是一个扭积表示定理——尽管带有浓厚的证明论色彩。