Publication
Structure Formation in Large Theories
Serge Autexier; Dieter Hutter
In: Cezary Kaliszyk (Hrsg.). Conference on Intelligent Computer Mathematics 2015. Conference on Intelligent Computer Mathematics (CICM-2015), July 13-17, Washington, DC, USA, Lecture Notes on Artificial Intelligence (LNAI), Springer, 7/2015.
Abstract
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.