QUIP-A Computational Framework for Advanced Reasoning Tasks

With the advent of large bodies of information sources like the internet, the importance of reasoning systems being able to handle rational decisions based on possibly inconsistent and incomplete information grows steadily. Research in artificial intelligence produced a number of well-established logic-based approaches dealing with various aspects of reasoning in underspecified domains (prominent among these methods are so-called "nonmonotonic logics``). Although these formalisms are extensively studied from a theoretical point of view, most of them lack implemented solvers. The reason for this can be explained by the fact that the majority of nonmonotonic formalisms have a higher computational complexity than classical reasoning. In this project, we plan to research methods for implementing various formalisms to reasoning in a dynamical domain based on a uniform approach. The basic idea is to translate each formalism into a common logical language for which efficient automated reasoning engines exist. The starting point will comprise formalisms dealing with nonmonotonic reasoning, but other formalisms (even more complicated ones) will be treated as well. The common logical basis will be given by the language of quantified boolean formulas (QBFs), which possess a suitable expressive power to deal with a large number of important knowledge representation tasks. As well, several successful QBF-solvers have been realized quite recently. We plan to study both suitable translations of reasoning tasks into QBFs and necessary adaptions and improvements of existing QBF algorithms. The result of the project will be an automated deduction framework which will serve as an experimental platform for rapid prototyping. The system will not only be beneficial for researching purposes, but can also serve as an educational tool at universities. Concerning the latter point, students will be able to experiment with different approaches thought at AI courses in a straightforward manner. Another important application area of the realized system will be possible usage as an inference engine in a multi- agent system hosting different kinds of intelligent agents. Such agents may respectively operate with different underlying reasoning strategies and our proposed system can handle the different kinds of queries in a uniform way.