Research report 2005 - Max Planck Institute for Informatics
Automatic Theorem Proving in Complex Theories
Logik der Programmierung (Prof. Dr. Harald Ganzinger)
MPI für Informatik, Saarbrücken
SummaryWe 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.