一种寻找极小不可满足子公式的方法

摘要：

用F表示经典命题逻辑的合取范式(CNF)公式,Gi为F中的子句.公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足.本文在经典命题逻辑中引入由F所诱导的形式背景,并基于此建立了概念格;给出了F不可满足公式的判定方法,当F为不可满足公式时,运用概念格的方法从F及其子句集的关系出发给出了F极小不相容子公式的判定定理.

关键词：合取范式、极小不可满足子公式、概念格

所属期刊栏目：14

分类号：O141(数理逻辑、数学基础)

资助基金：陕西省教育厅自然科学研究项目09JK722;西安邮电学院中青年项目105-0460

在线出版日期：2009-11-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：144-147