Uwe Egly, Thomas Eiter, Hans Tompits, and Stefan Woltran, Technische Universität Wien
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.