不可满足公式的完备证明系统(英文)

合取范式(CNF)公式H到F的同志是一个从H的文字集合到F的文字集合的映射、并保持补运算和子句映到子句。同态映射保持一个公式的不可满足性。一个公式是极小不可满足的是指公式不可满足而且从中删去任一个子句后得到的公式可满足。MU(1)是子句数与变元数的差等于1的极小不可满足公式类。S.Szeider证明了:每个不可满足公式F是MU(1)中某个公式H的同态像。从而,基于MU(1)的同态证明系统与树消解证明系统是P—等价的。MU(1)中的公式可以用基础矩阵表示,本文用基础矩阵的方法证了同态证明系统Ⅱ_(MU(1))的完备性。