@techreport{ea16228037c64a248f720cad4c2f0fcf,
title = "Knowledge Archives in Theorema: A Logic-Internal Approach",
abstract = "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.",
author = "Camelia Rosenkranz and Bruno Buchberger and Tudor Jebelean",
year = "2009",
month = jan,
language = "English",
series = "RISC Report Series",
publisher = "RISC, JKU-Linz",
number = "09-01",
type = "WorkingPaper",
institution = "RISC, JKU-Linz",
}