Stellar Resolution：乘法
Stellar Resolution: Multiplicatives
摘要：
我们提出了一个新的异步计算模型命名为恒星分辨率的基础上一阶统一。这个模型的计算是作为一个正式的吉拉德的先验语法程序，勾画了一系列的三篇文章。因此，这是第一步，以适当的正式处理吉拉德的建议，以解决一阶逻辑的证明程序的方法。在建立了恒星分辨率的形式定义和基本性质之后，我们解释了它是如何推广传统的计算模型的，例如逻辑编程和组合模型，例如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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
