论文标题
来自基于分辨率的瓷砖系统的乘法线性逻辑
Multiplicative linear logic from a resolution-based tile system
论文作者
论文摘要
我们提出了恒星分辨率，这是基于鲁滨逊的一阶分辨率的“灵活”瓷砖系统。在建立了恒星分辨率的形式定义和基本特性之后，我们展示了其图林的完整性并说明模型，我们展示了它如何自然地代表Horn Crauses和and Automata以及在DNA计算中使用的非确定瓷砖结构。在第二个和主要部分中，通过使用恒星解决方案，我们将吉拉德（Girard）在他的超越语法计划中概述的证明网络理论的新替代方案形式化和扩展。特别是，我们为线性逻辑（MLL）的乘法片段编码切割和逻辑正确性。最终，我们通过所谓的混合规则获得了MLL和MLL的完整性结果。通过扩展吉拉德（Girard）相互作用的几何形状的想法，这提出了对逻辑与计算之间相互作用的新了解的第一步，在该逻辑和计算之间，线性逻辑被视为格式化计算的（构造）方法。
We present the stellar resolution, a "flexible" tile system based on Robinson's first-order resolution. After establishing formal definitions and basic properties of the stellar resolution, we show its Turing-completeness and to illustrate the model, we exhibit how it naturally represents computation with Horn clauses and automata as well as nondeterministic tiling constructions used in DNA computing. In the second and main part, by using the stellar resolution, we formalise and extend ideas of a new alternative to proof-net theory sketched by Girard in his transcendental syntax programme. In particular, we encode both cut-elimination and logical correctness for the multiplicative fragment of linear logic (MLL). We finally obtain completeness results for both MLL and MLL extended with the so-called MIX rule. By extending the ideas of Girard's geometry of interaction, this suggests a first step towards a new understanding of the interplay between logic and computation where linear logic is seen as a (constructed) way to format computation.
