The goal of this project, supported by the Austrian Research Fund (FWF), is to investigate methods for implementing various formalisms for knowledge representation and reasoning (KR) in a single framework. Problem specifications based on more than one KR formalism will be supported within this framework. The common basis of all methods are quantified Boolean formulas (QBFs). Suitable translations of KR problems into QBFs and inference principles for QBFs will be researched, and their feasibility will be examined on particular applications.
The result will be an automated deduction framework which will serve as an experimental platform for rapid prototyping. This system will be beneficial for KR researchers and will also support educational purposes at universities.
Designing automated inference systems for KR formalisms (like, e.g., nonmonotonic reasoning) is challenged by the increased computational complexity compared to the inherent complexity of classical reasoning. As is well known, the main reasoning tasks for major propositional nonmonotonic inference principles are located at the second level of the polynomial hierarchy, whereas classical propositional satisfiability and provability reside at the first level of that hierarchy, i.e., they are complete for the well-known complexity classes NP and co-NP. Moreover, many reasoning tasks, for instance provability in certain propositional modal logics, are even more involved by being PSPACE-complete.
The lack of sophisticated implementations for nonmonotonic reasoning is one reason why research was focused nearly exclusively on theoretical investigations. In the last few years, we have seen a few monolithic implementations available which focus on KR problems from the first or second level of the polynomial hierarchy, e.g., DLV. These systems are limited in the sense that they can efficiently represent problems from the second level of the polynomial hierarchy, but, for harder problems, the representation becomes exponential in general. The availability of sophisticated implementations like DLV or smodels has caused an increasing interest in nonmonotonic reasoning, and especially in answer set programming, because these two tools implement this kind of reasoning. Efficient and publicly available tools stimulate more practicably oriented research by allowing easy experimentation.
The intended system QUIP is an automated deduction system for many problems in AI and knowledge representation like the following ones:
Our proposed approach is based on the reduction of problems from the polynomial hierarchy into QBFs, which are then evaluated by a QBF-solver. The practical feasibility of this idea is witnessed by the increasing number of available systems for evaluting QBFs. (For an uptodate web-resouce QBFLIB is highly recommended.)
The first goal is to find reductions of KR problems into QBFs. The existence of reductions from KR problems to appropriate QBFs follows immediately from the membership of the KR problems with respect to a specific complexity class and the hardness of the appropriate QBFs with respect to that class. The construction of such a reduction is a non-trivial task. For syntactically restricted instances of KR problems specifically tailored reductions will be developed.
The next step is then the evaluation of such reductions comparing different available QBF-solvers. One goal is to examine the strengths and weaknesses of the particular solvers, together with the translation procedures into the required normal forms. The assumed result is a characterization under which circumstances which QBF-solvers should be preferred.
Based on the reductions, the implementation of the framework is intended to be a platform well suited for experiments with different KR principles. The resulting systems should
(Information for students - only in German.)