一些命题逻辑中的双重否定消除
摘要：没有双重否定的证明的存在保证的条件条件以及具有双重否定的自由结论的定理的存在性的条件 确保存在于没有双重否定的结论的情况下，保证没有双重否定的证明存在的条件 关于经典命题演算的公理系统的存在性，如果结论没有双重否定，则使用该公理系统保证了没有双重否定的证明的存在性 对第一个问题给出条件的回答之后，我们通过关注Lukasiewicz三公理系统来回答第二个问题 然后我们扩展我们的研究到无穷值命题演算和直觉逻辑，并推广了没有双重否定的概念 感兴趣的双重否定证明完全依赖于推理规则紧凑剥离，一种将模态浅陷与适当的广义替换规则相结合的规则 自动推理程序OTTER在这项研究中发挥了不可或缺的作用
作者：Michael Beeson, Robert Veroff, Larry Wos
论文ID：cs/0301026
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23