论文部分内容阅读
对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向。极小不可满足公式通过分裂得到的公式保持了极小不可满足性,它的子类的某些性质对于建立在分裂上的归纳证明是很有用的。找到了一个能递归构造的极小不可满足公式的子类MAX＋,并证明这种递归构造方法具有可靠性和完备性,最后给出了一个构造实例。