将"Adding Negation to Lambda Mu"翻译成中文为："向Lambda Mu添加否定"
摘要：$lambdamu$-演算是Parigot的演算的扩展，通过添加否定作为类型构造器，以及表示否定引入和消除的语法构造。我们将定义一个扩展了$lambdamu$的规约系统的规约概念，其中包含两条新的规约规则，并证明该系统满足主题约简性。使用Aczel对Tait和Martin-L"of并行约简概念的概括，我们证明了这种扩展的约简是可合流的。尽管类型赋值的概念在表示自然演绎中的蕴含和否定的证明方面存在一些限制，但我们将证明所有在其中可以证明的命题在$cal L$中都有一个证明实例。使用Girard的可约性候选方法，我们证明所有可类型化的项都是强正规型的，并在论文的结尾展示了$cal L$类型赋值具有主类型属性。
作者：Steffen van Bakel
论文ID：2109.10447
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-25