RISC Forum

Retrieval and Structuring of Large Mathematical Knowledge Bases in Theorema

Camelia Rosenkranz

Abstract

In this thesis we develop a Theorema approach to Mathematical Knowledge Management (MKM) for the working mathematician. Mathematical knowledge archives are introduced as an extension of Theorema, allowing the representation of large bodies of mathematics with their inherent structure. Various logic–internal constructs for building archives in a natural way are presented: breaking formulae across cells, grouping them in a hierarchy, attaching labels to subhierarchies, disambiguating symbols by namespaces, importing symbols from other namespaces, describing categories and functors via namespaces. All these constructs are logic–internal in the sense that they have a natural translation to higher–order logic so that various operations of MKM can be carried out in the object logic itself. In addition to input/output commands, operations for restructuring archives and the translation to plain Theorema are implemented; the latter provides a rigorous semantics of the archive language. As an alternative to user input, archives can also be expanded by theory exploration mechanisms. Retrieval, a central topic of MKM, is treated in connection with theorem proving and algorithm synthesis. Two main types of retrieval are distinguished: syntactic and semantic. While syntactic retrieval employs textual search techniques, matching, and unification between the target formula and the knowledge base, semantic retrieval obtains the target formula from the knowledge base by applying basic inference steps. The Theorema commands implementing various flavors of retrieval are presented. As a larger example of an archive, we have formalized a chapter on lattice theory taken from a standard algebra textbook.

ThesisCR.pdf (1MB)