[Back]

S. Woltran:
"A Framework for Solving Advanced Reasoning Tasks - Summary of the Thesis";
ÖGAI Journal, 21 (2002), 4; 29 - 33.

Although there are many arguments that logic is an appropriate tool for artificial intelligence, there has been a perceived problem with the monotonicity of classical logic: Human intelligence is capable of drawing conclusions, acting on them, and then retracting them if necessary in the face of new evidence. But in contrast, conventional deduction in classical logic forces conclusions to remain valid if the set of premises is enlarged. Hence, advanced reasoning principles, often referred to as nonmonotonic reasoning, circumventing this weakness are fundamental in designing intelligent systems.

In the thesis we present both theoretical foundations and a concrete implementation of a mechanism providing a uniform methodology for a wide array of different formalizations of nonmonotonic reasoning. The theoretical basis is derived from well-known results about the computational complexity of nonmonotonic logics and exploits a reduction of the different reasoning tasks to the evaluation of quantified Boolean formulas (QBFs). These reductions
have been used to develop the system QUIP, which is built on top of practicably efficient QBF-solvers. To the best of our knowledge, QUIP is the first framework, which is able to handle all important nonmonotonic logics in reasonable performance.