不可满足公式的完备证明系统

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

Complete Proof Systems for Unsatisfiable Formulas

A homomorphism ψ of CNF formulas from H to F is a function mapping the set of liter-als in H to the set of literals in F and it preserves complements and clauses. If the formula H ishomomorphic to the formula F, then the unsat isfiability of H implies the unsatisfiability of F. ACNF formula F is minimal unsatisfiable if F is unsatisfiable and the resulting formula deleting any-one clause from F is satisfiable. MU( 1 ) is a class of minimal unsatisfiable formulas with the defi-ciency of the number of clauses and variables to be one. S. Szeider proved that for each unsatisfi-able formula F there exists a formula H in MU( 1 ) and ahomomorphism ψ: H→F. Whence, theproof system based on homomorphism from MU (1) and the tree resolution proof system arep-equivalent.A MU( 1 ) formula can be represented by basic matrix. In this paper, we present a new proofof the completeness of the proof system ∏MU(1) by the method of basic matrix.