交互与结构系统
摘要：通过非交换的自对偶逻辑运算符扩展乘法线性逻辑，本论文引入了一种逻辑系统称为BV。这种扩展对序量演算来说尤为具有挑战性，到目前为止尚未在其中实现。在名为结构演算的新形式主义下，这种扩展变得非常自然，结构是受到序量的特定等式法则约束的公式。结构演算通过将序量演算广义化，以观察到导出的新的自顶向下对称性，并且它采用了在任何深度重写结构内部的推理规则。这些特性除了允许设计BV之外，还产生了一个模块化的削减切除证明。
作者：Alessio Guglielmi
论文ID：cs/9910023
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23