Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas

Abstract

We consider the compilation of different reasoning tasks into the evaluation problem of quantified boolean formulas (QBFs) as an approach to develop prototype reasoning sys-tems useful for, e.g., experimental purposes. Such a method is a natural generalization of a similar technique applied to NP-problems and has been recently proposed by other re-searchers. More specifically, we present translations of sev-eral well-known reasoning tasks from the area of nonmono-tonic reasoning into QBFs, and compare their implementa-tion in the prototype system QUIP with established NMR-provers. The results show reasonable performance, and docu-ment that the QBF approach is an attractive tool for rapid pro-totyping of experimental knowledge-representation systems.