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