Structure formation in large theories

DOI10.1007/978-3-319-20615-8_10MaRDI QIDQ3453112zbMATH OpenOpenAlexFDO

Authors Serge Autexier, Dieter Hutter

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1505.01620

Mathematics Subject Classification ID

Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

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.

Recommendations

• Building Structured Theories
• An abstraction-refinement framework for reasoning with large theories
• Theorem proving with structured theories. (Preliminary report)
• scientific article; zbMATH DE number 2079992
• Sine qua non for large theory reasoning

Cites work

• Development graphs -- proof management for structured specifications
• Extended Formula Normalization for ε-Retrieval and Sharing of Mathematical Knowledge
• Institutions: abstract model theory for specification and programming
• Matching concepts across HOL libraries
• The TPTP World -- infrastructure for automated reasoning

Cited in

(5)

• Approximate theory of large-scale structure formation in dark matter
• scientific article; zbMATH DE number 1614690 (Why is no real title available?)
• scientific article; zbMATH DE number 2079992 (Why is no real title available?)
• The maximum sizes of large scale structures in alternative theories of gravity
• Structure formation beyond shell-crossing: nonperturbative expansions and late-time attractors

Describes a project that uses

Uses Software

• MAYA
• TPTP
• Mizar

This page was built for publication: Structure formation in large theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453112)