Reasoning in Complex Theories and Applications

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