As the ontology component, we consider extensions of the DL ALC, allowing for transitive The use of ontologies to provide background knowledge closure of roles. The study of finite entailment is relevant for enriching answers to queries posed to a database is a for this combination because, unlike for plain CQs, query major research topic in the fields of knowledge representation entailment of CQs with transitive closure is not finitely controllable and reasoning. In this data-centric setting, various even for ALC, and thus finite and unrestricted entailment options for the formalisms used to express ontologies and do not coincide. As a consequence, dedicated algorithmic queries exist, but popular choices are description logics methods and lower bounds need to be developed.

Many important problems can be compactly represented as quantified boolean formulas (QBF) and solved by general QBF solvers. To date QBF solvers have mainly focused on determining whether or not the input QBF is true or false. However, additional important information about an application can be gathered from its QBF formulation. In this paper we demonstrate that a circuit-based QBF solver can be exploited to obtain a Q-Resolution proof of the truth or the falsity of a QBF. QBFs have a natural interpretation as a two person game and our main result is to show how, via a simple computation, the moves for the winning player can be computed directly from these proofs. This result shows that the proof is a representation of the winning strategy. In previous approaches the winning strategy has often been represented in a way that makes it hard to verify. In our approach the correctness of the strategy follows directly from the correctness of the proof, which is relatively easy to verify.