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

【Abstract】 Let F be the conjunction normal form(CNF formula),Ci be the clause of F in classical propositional logic system.A CNF formula F is minimally unsatisfiable if F is unsatisfiable,and the resulting formula that is deleted any one clause from F is satisfiable.In this paper, by introducing the formal context induced by F,the concept lattices are built based on the formal context induced by F,and several ways to determine whether the formula F is satisfiable or not are studied;several ways to explore minimal unsatisfiable subformula of F by the concept lattice theory are given.更多还原