Project: QUIP - A Computational Framework for Advanced Reasoning Tasks
(supported by the Austrian Science Foundation under grant P15068.)
Contents
- Project team
- Goal of the project
- Motivation and background
- Goals of the research
- Publications
- Related courses at our department
Project team
Students:
- Volker Klotz
- Martina Seidl
- Michael Zolda
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:
- Propositional nonmonotonic reasoning principles: Prominent nonmonotonic formalisms are default logic, circumscription, and autoepistemic logic.
- logic-based abduction;
- belief revision
- propositional reasoning in constructive logics; for instance, equilibrium logic which is a generalization of answer set programming;
- paraconsistent reasoning
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
- be easily extensible to new KR formalisms;
- provide an intuitive user interface together with explanation capabilities in order to present results in the ``language of the problem description'' and not in terms of the internal problem representation;
- support students when they try to understand basic KR principles and experiment with different KR formalisms; and
- be reasonable with respect to the performance of highly sophisticated special purpose implementations.
Publications
- D. Pearce, H. Tompits, and S. Woltran "Encodings for Equilibrium Logic and Logic Programs with Nested Expressions", EPIA-01, Springer 2001. (... .ps.gz)
- J. Delgrande, T. Schaub, H. Tompits, and S. Woltran "On Computing Solutions to Belief Change Scenarios", ECSQARU-01, Springer 2001. (... .ps.gz)
- U. Egly, T. Eiter, V. Klotz, H. Tompits, and S. Woltran "A Toolbox for Abduction: Preliminary Report", Proceedings ICJAR-Workshop QBF-01, 2001. (... .ps.gz)
- U. Egly, T. Eiter, R. Feldmann, S. Schamberger, H. Tompits, and S. Woltran "On Mechanizing Modal Nonmonotonic Logics", Proceedings DGNMR-01, 20001. (... .ps.gz)
- U. Egly, T. Eiter, V. Klotz, H. Tompits, and S. Woltran "Computing Stable Models with Quantified Boolean Formulas: Some Experimental Results", Proceedings AAAI 2001 Spring Symposium, AAAI Press 2001. (... .ps.gz)
- U. Egly, T. Eiter, H. Tompits, and S. Woltran "Solving Advanced Reasoning Tasks using Quantified Boolean Formulas", AAAI-00, AAAI Press 2000. (... .ps.gz)
- U. Egly, T. Eiter, H. Tompits, and S. Woltran "QUIP - A Tool for Computing Nonmonotonic Reasoning Tasks", Proceedings, NMR-00, 2000. (... .ps.gz)
Related courses at our department
(Information for students - only in German.)