Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas

We consider the compilation of different reasoning tasks into the evaluation problem of quantified boolean formulas (QBFs) as an approach to develop prototype reasoning systems 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 researchers. More specifically, we present translations of several well-known reasoning tasks from the area of nonmonotonic reasoning into QBFs, and compare their implementation in the prototype system QUIP with established NMRprovers. The results show reasonable performance, and document that the QBF approach is an attractive tool for rapid prototyping of experimental knowledge-representation systems.

• Type: Conference
• Year: 2000
• Where: AAAI
• Authors: Uwe Egly, Thomas Eiter, Hans Tompits, Stefan Woltran
• Keywords: AAAI 2000, Intelligent Agents, Prototype Reasoning Systems, Reasoning Tasks, Well-known Reasoning Tasks