Research report 2005 - Max Planck Institute for Informatics

Automatic Theorem Proving in Complex Theories

Sofronie-Stokkermans, Viorica

Logik der Programmierung (Prof. Dr. Harald Ganzinger)
MPI für Informatik, Saarbrücken

We identify situations in which it is possible to decompose proof tasks in complex theories in a modular way into proof tasks for the simpler components of these theories. As they exploit modularity, such proof procedures are especially flexible and efficient and are therefore widely applicable, for instance in the verification of complex systems, but also in mathematics or knowledge representation.

For the full text, see the German version.

Zur Redakteursansicht