不可满足公式的完备证明系统

来源 :贵州大学学报：自然科学版 | 被引量 : 0次 | 上传用户：yangclio

【摘要】

：

合取范式(CNF)公式H到F的同态是一个从H的文字集合到F的文字集合的映射、并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指公式

【作者】

：

许道云

【机构】

：

贵州大学计算机科学系

【出处】

：

贵州大学学报：自然科学版

【发表日期】

：

2003年3期

【关键词】

：

不可满足公式同态证明 NP—完全性 unsatisfiable formulas homomorphism proof NP-completeness

【基金项目】

：

贵州省自然科学基金，贵州省教育厅自然科学基金

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

合取范式(CNF)公式H到F的同态是一个从H的文字集合到F的文字集合的映射、并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指公式不可满足而且从中删去任一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.S.Szeider证明了:每个不可满足公式F是MU(1)中某个公式H的同态像.从而,基于MU(1)的同态证明系统与树消解证明系统是p-等价的.MU(1)中的公式可以用基础矩阵表示,本文用基础矩阵的方法证了同态证明系统∏MU(1)的完

其他文献

河南灵宝成功举办2013中国苹果年会

9月24日上午，2013中国苹果年会暨三门峡灵宝苹果博览会在灵宝市隆重开幕。河南省副省长王铁，中国果品流通协会会长赵显人，市委副书记、市长赵海燕等领导出席会议。本次年会由中

期刊

河南省苹果中国年会人民政府三门峡市会员单位专业合作社

山药多酚的功能及开发应用展望

本文介绍了山药及其多酚的组成,论述了山药多酚的功能并对山药的应用进行了展望。

期刊

山药多酚功能Yam poly-phenols function

二期梅毒误诊为寻常型银屑病1例报告

1 病例患者李某,男,38岁,已婚.因双侧腋下、胸、腹部及两大腿内侧较多黄豆大,玫瑰色丘疹半年余,曾到本区多家医院就诊,诊断为"寻常型银屑病",但治疗无效.患者本人否认非婚性

期刊