History


Please fill in your query. A complete syntax description you will find on the General Help page.
Resolution on quantified generalized clause-sets. (English)
J. Satisf. Boolean Model. Comput. 7, No. 1, 17-34 (2010).
Summary: 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 can also be considered as a generalization of Q-resolution for quantified Boolean CNF formulae (QCNF).
WorldCat.org
Valid XHTML 1.0 Transitional Valid CSS!