Skip to Content

TU Wien Fakultät für Informatik KBS Knowledge-Based Systems Group
Top-level Navigation: Current-level Navigation:

Path: KBS > research > projects > quip >

Tools: Drucken

Project: QUIP - A Computational Framework for Advanced Reasoning Tasks

(supported by the Austrian Science Foundation under grant P15068.)


Project team


Goal of the project

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.

Motivation and background

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:

For some of the above topics, special-purpose implementations are available, which do not rely on a general inference engine. In each of these implementations, the complete machinery is implemented from scratch. There is no methodology for the combination of different kinds of reasoning within a general framework in the literature. The advantage of such a framework on the implementation side is reuse of software; only the reduction for the problem under consideration has to be implemented but the underlying inference engine (i.e., the QBF-solver) remains unchanged. Consequently, this simplifies implementation of new reasoning tasks.

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.)

Goals of the research

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


Related courses at our department

(Information for students - only in German.)

Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist die Fakultät für Informatik an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. / Disclaimer.