Resolution on Quantified Generalized Clause-sets.

This paper is devoted to investigate resolution for quantified generalized clause-sets (QCLS). The soundness and refutation completeness are proved. Then quantified generalized Horn clause-sets are introduced for which a restricted resolution, called quantified positive unit resolution, is proved to be sound and refutationally complete. Moreover, it is shown that the satisfiability for quantified generalized Horn clause-sets is solvable in polynomial time. On the one hand, the work of this paper can be considered as a generalization of resolution for generalized clause-sets (CLS). On the other hand, it also can be considered as a generalization of Q-resolution for quantified boolean CNF formulae (QCNF).

• Type: Journal
• Year: 2010
• Where: JSAT
• Authors: Jiwei Jin, Xishun Zhao
• Keywords: Boolean Cnf Formulae, Horn Clause-sets, JSAT 2010, Positive Unit Resolution