一个极小不可满足公式子集的构造  

A Structure of Minimal Unsatisfiable Formulas Subsets

作　　者：陈庆燕[1] 姚雷博[2] 

机构地区：[1]滨州学院计算机系,山东滨州256600 [2]洛阳理工学院电气工程与自动化系,河南洛阳471023

出　　处：《洛阳理工学院学报（自然科学版）》2011年第4期77-79,87,共4页Journal of Luoyang Institute of Science and Technology：Natural Science Edition

基　　金：滨州学院青年人才创新基金(BZXYQNLG200611)

摘　　要：对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向。极小不可满足公式通过分裂得到的公式保持了极小不可满足性,它的子类的某些性质对于建立在分裂上的归纳证明是很有用的。找到了一个能递归构造的极小不可满足公式的子类MAX+,并证明这种递归构造方法具有可靠性和完备性,最后给出了一个构造实例。Research on minimal unsatisfiable formulas and its subclasses is an active topic that begins to spring up in recent years. The splitting of formulas in minimal unsatisfiable formulas remains minimal unsatisfiability and some properties of the subclass are very useful for induction proofs based on the splitting technique. In this paper, it proposes a subset MAX＇of constructing recursively minimal unsatisfiable formulas and proves that the method is complete and sound, at last it gives a structural example.

关 键 词：极小不可满足公式 MAX+(k)公式集 分裂对 

分 类 号：TP301.5[自动化与计算机技术—计算机系统结构]