Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas
Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas
复制标题
DOI：
--
复制
发表时间：
2000-07
期刊：
影响因子：
--
通讯作者：
Uwe Egly;Thomas Eiter;H. Tompits;S. Woltran
中科院分区：
文献类型：
--
作者：
Uwe Egly;Thomas Eiter;H. Tompits;S. Woltran
我们考虑将不同的推理任务编译成量化布尔公式（QBF）的评估问题，作为开发原型推理系统的一种方法，例如，实验目的。这样的方法是一个自然的推广类似的技术应用于NP问题，最近已提出了其他研究人员。更具体地说，我们提出了翻译的几个著名的推理任务，从该地区的非单调推理到QBF，并比较它们的实现在原型系统QUIP与建立NMRprovers。结果表明，合理的性能，和文件的QBF方法是一个有吸引力的工具，实验知识表示系统的快速原型。
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.