Structure Formation in Large Theories
This work addresses the challenge of managing and reasoning with large theories in formal methods, but it appears incremental as it builds on existing development graph concepts.
The paper tackles the problem of combinatorial explosion in reasoning over large theories by transforming flat theories into structured development graphs, resulting in more structured and concise theories as demonstrated with MIZAR articles in TSTP-representations.
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.