2007/08/30 by Paolo Liberatore, Liberatore, Paolo
Computer Science · #AI-based Problem Solving and Planning #Artificial Intelligence (cs.AI) #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.AI #cs.CC #cs.LO
paper · pdf · doi:10.48550/arxiv.0708.4170
arxiv created 2007/08/30 · openalex publication_date 2007/08/30 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This article presents a technique for proving problems hard for classes of the polynomial hierarchy or for PSPACE. The rationale of this technique is that some problem restrictions are able to simulate existential or universal quantifiers. If this is the case, reductions from Quantified Boolean Formulae (QBF) to these restrictions can be transformed into reductions from QBFs having one more quantifier in the front. This means that a proof of hardness of a problem at level n in the polynomial hierarchy can be split into n separate proofs, which may be simpler than a proof directly showing a reduction from a class of QBFs to the considered problem.