Resolution for quantified Boolean formulas. (English) Zbl 0828.68045

Kleine Büning, Hans; Karpinski, Marek; Flögel, Andreas

Inf. Comput. 117, No. 1, 12-18 (1995).

Summary: A complete and sound resolution operation directly applicable to the quantified Boolean formulas is presented. If we restrict the resolution to unit resolution, then the completeness and soundness for extended quantified Horn formulas is shown. We prove that the truth of a quantified Horn formula can be decided in \(O(rn)\) time, where \(n\) is the length of the formula and \(r\) is the number of universal variables, whereas in contrast the evaluation problem for extended quantified Horn formulas is coNP-complete for formulas with prefix \(\forall\exists\). Further, we show that the resolution is exponential for extended quantified Horn formulas.

MSC:

68N17	Logic programming
68Q25	Analysis of algorithms and problem complexity
03D40	Word problems, etc. in computability and recursion theory

Keywords:

quantified Boolean formulas; quantified Horn formulas