Publikation

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 United States Lecture Notes on Artificial Intelligence (LNAI) Springer 7/2015.

Abstrakt

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.

Projekte

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