Structure Formation in Large Theories

Serge Autexier, Dieter Hutter

In: Cezary Kaliszyk (editor). Conference on Intelligent Computer Mathematics 2015. Conference on Intelligent Computer Mathematics (CICM-2015) July 13-17 Washington DC United States Lecture Notes on Artificial Intelligence (LNAI) Springer 7/2015.


Structuring theories is one of the main approaches to reduce the combinatorial explosion associated with reasoning and exploring large theories. In the past we developed the notion of development graphs as a means to represent and maintain structured theories. In this paper we present a methodology and a resulting implementation to reveal the hidden structure of flat theories by transforming them into detailed development graphs. We review our approach using plain TSTP-representations of MIZAR articles obtaining more structured and also more concise theories.


German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz