Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.