论文标题
恒星分辨率：乘法
Stellar Resolution: Multiplicatives
论文作者
论文摘要
我们提出了一种基于一阶统一的恒星分辨率的新型计算模型。该计算模型是作为吉拉德（Girard）的超验语法程序的形式化，该计划在一系列三篇文章中概述。因此，这是朝着对吉拉德（Girard）提出的提案进行正式待遇的第一步，该提议在证明的方法中解决了一阶逻辑。在建立了恒星解决方案的形式定义和基本属性之后，我们解释了它如何概括传统的计算模型，例如逻辑编程和组合模型，例如Wang Tilings。然后，我们解释了它如何表示乘法证明结构，其切割和Danos和Regnier的正确性标准。在相互作用模型的先前几何形状之后，进一步使用可真实性技术会导致乘法线性逻辑的动态语义。
We present a new asynchronous model of computation named Stellar Resolution based on first-order unification. This model of computation is obtained as a formalisation of Girard's transcendental syntax programme, sketched in a series of three articles. As such, it is the first step towards a proper formal treatment of Girard's proposal to tackle first-order logic in a proofs-as-program approach. After establishing formal definitions and basic properties of stellar resolution, we explain how it generalises traditional models of computation, such as logic programming and combinatorial models such as Wang tilings. We then explain how it can represent multiplicative proof-structures, their cut-elimination and the correctness criterion of Danos and Regnier. Further use of realisability techniques lead to dynamic semantics for Multiplicative Linear Logic, following previous Geometry of Interaction models.
