| 一种寻找极小不可满足子公式的方法 |
| |
| 引用本文： | 李立峰.一种寻找极小不可满足子公式的方法[J].西安邮电学院学报,2009,14(5):144-147. |
| |
| 作者姓名： | 李立峰 |
| |
| 作者单位： | 西安邮电学院应用数理系,陕西,西安710121 |
| |
| 基金项目： | 陕西省教育厅自然科学研究项目，西安邮电学院中青年项目 |
| |
| 摘 要： | 用F表示经典命题逻辑的合取范式(CNF)公式,Ci为F中的子句。公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足。本文在经典命题逻辑中引入由F所诱导的形式背景,并基于此建立了概念格;给出了F不可满足公式的判定方法,当F为不可满足公式时,运用概念格的方法从F及其子句集的关系出发给出了F极小不相容子公式的判定定理。
|
| 关 键 词： | 合取范式 极小不可满足子公式 概念格 |
A method to explore the minimal unsatisfiable subformula |
| |
| LI Li-feng.A method to explore the minimal unsatisfiable subformula[J].Journal of Xi'an Institute of Posts and Telecommunications,2009,14(5):144-147. |
| |
| Authors: | LI Li-feng |
| |
| Affiliation: | LI Li- feng (Department of Applied Mathematics and Physics, Xi＇an University of Posts and Telecommunications, Xi＇an 710121,China) |
| |
| 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 suhformula of F by the concept lattice theory are given. |
| |
| Keywords: | conjunction normal form minimal unsatisfiable subformula concept lattice |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
