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

Complete Proof Systems for Unsatisfiable Formulas

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

A homomorphism of CNF formulas from H to F is a function mapping the set of literals in H to the set of literals in F and it preserves complements and clauses. If the formula H is homomorphic to the formula F, then the unsat isfiability of H implies the unsatisfiability of F. A CNF formula F is minimal unsatisfiable if F is unsatisfiable and the resulting formula deleting anyone clause from F is satisfiable. MU( 1) is a class of minimal unsatisfiable formulas with the deficiency of the number of clauses and variables to be one. S. Szeider proved that for each unsatisfiable formula F there exists a formula H in MU( 1) and ahomomorphism : H→F. Whence, the proof system based on homomorphism from MU ( 1 ) and the tree resolution proof system are p-equivalent. A MU{ 1) formula can be represented by basic matrix. In this paper, we present a new proof of the completeness of the proof system ПMU(1) ky the method of basic matrix.