Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Nonmonotonic Reasoning

We consider compiling reasoning tasks into the evaluation problem of Quantified Boolean Formulas (QBFs) which are useful as an approach to develop prototype reasoning systems for experimental purposes. Such a method has been recently proposed by other researchers, who provided algorithms for evaluating QBFs. However, these algorithms require input formulas in prenex clausal normal form. In this paper, we complement these investigations by describing a framework, QUIP, which handles arbitrary QBFs. QUIPs reasoning engine is boole, an evaluator for QBFs based on binary decision diagrams (BDDs). We present translations of several well-known reasoning tasks from the area of nonmonotonic reasoning (NMR) into QBFs, and compare their implementation in QUIP with established NMR-provers. The results show reasonable performance, and document that the QBF approach is an attrative tool for rapid prototyping of experimental KR systems.