不可满足公式的同态证明系统

• 作者: 许道云
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 不可满足公式 同态 证明系统 基础矩阵 完备性
• 年，卷（期）: 2005,（3）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 336-345
• 页数: 10页
• 分类号: TP301
• 字数: 10130字
• 语种: 中文

摘要

合取范式(CNF)公式H到F的同态(是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	许道云	贵州大学计算机科学系	125	460	12.0	16.0