Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas
Uwe Egly, Thomas Eiter, Hans Tompits, Stefan Woltran · 2000
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.