Abstract
One of the most important objectives of the research in mathematics and
computer science is to obtain means of reasoning in and about complex systems.
These can be, for instance complex mathematical theories; programs, or
generally reactive or hybrid systems; distributed databases; or complex systems
in general (e.g. multi-agent systems or reactive or hybrid systems with
embedded software, whose behavior is controlled by databases, reasoning about
knowledge and belief, planning mechanisms, or programs). Proving that such
systems have certain properties (e.g. that they are safe, that they behave
correctly, or that the information they use does not contain inconsistencies)
is extremely important: In safety-critical systems (such as cars, trains,
planes, or power-plants) even small mistakes can provoke disasters. Since the
amount of data which has to be handled in verification tasks is usually huge,
computer support is indispensable. The dream of the scientists is to provide
such correctness proofs automatically. This goal cannot be reached in its full
generality: As shown by undecidability results going back to the work of Gödel,
Church and Turing, it is impossible to write a program for checking arbitrary
properties of general systems. However, for concrete application domains,
automatic procedures exist. It is therefore very important to identify
situations in which automated verification of complex systems is possible. For
this, it is essential to identify theories which are decidable, preferably with
low complexity, and - since concrete problems often are quite heterogeneous in
nature - to obtain methods for efficiently combining decision procedures.
The goal of the tutorial is to give a comprehensive, in-depth perspective of
recent advances in the field of reasoning in complex logical theories, and to
present applications of these results in various areas ranging from formal
verification to reasoning about knowledge. The tutorial introduces the general
principles underlying reasoning in complex theories from a unifying
perspective, gives a survey of recent achievements in the field, and
illustrates the problems and their solutions using a selection of examples from
mathematics, verification, and knowledge representation.
