You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Resolution on Quantified Generalized Clause-sets

Article type: Research Article

Authors: Jin, Jiwei; * | Zhao, Xishun

Affiliations: Institute of Logic and Cognition, Sun Yat-sen University, People’s Republic of China. E-mails: [email protected], [email protected]

Note: [*] Research was partially supported by the NSFC projects under Grant No.60970040 and a MOE project under Grant No. 05JJD72040122.

Keywords: quantified generalized clause-sets, satisfiability, Q-resolution, Horn

DOI: 10.3233/SAT190073

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 1, pp. 17-34, 2010

Received 1 July 2009
|
Revision received 1 November 2009
|
Published: 1 March 2010
Get PDF open access

Abstract

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).

Show more