Camelia Rosenkranz, Bruno Buchberger, Tudor Jebelean,
"Knowledge Archives in Theorema: A Logic-Internal Approach"
, Serie RISC Report Series, University of Linz, Austria, Nummer 09-01, RISC, JKU Linz, Schloss Hagenberg, 4232 Hagenberg, 1-2009
Knowledge Archives in Theorema: A Logic-Internal Approach
Sprache des Titels:
Archives are implemented as an extension of Theorema for representing mathematical repositories in a natural way. An archive can be conceived as one large formula in a language consisting of higher-order predicate logic together with a few constructs for structuring knowledge: attaching labels to subhierarchies, disambiguating symbols by the use of namespaces, importing symbols from other namespaces and specifying the domains of categories and functors as namespaces with variable operations. All these constructs are logic-internal in the sense that they have a natural translation to higher-order logic so that certain aspects of Mathematical Knowledge Management can be realized in the object logic itself. There are a variety of operations on archives, though in this paper we can only sketch a few of them: knowledge retrieval and theory exploration, merging and splitting, insertion and translation to predicate logic.