一种可扩展的模块系统
A Scalable Module System
摘要：
从计算机代数系统到定理证明器的符号和逻辑计算系统正在进入科学、技术、数学和工程领域。但是这样的系统依赖于显式或隐式表示的数学知识，需要管理这些知识才能有效地使用这样的系统。虽然数学知识管理（MKM）“在小”是很好的研究，扩大到大型，高度互联的语料库仍然很困难。我们认为，为了实现MKM“在大”，我们需要的表示语言和软件架构，系统地设计与大规模处理的想法。为此，我们设计并实现了数学理论模块系统MMT语言。MMT被设计为最简单的语言，它结合了模块系统，基本未提交的形式语义和Web可扩展的实现。由于仔细选择的代表性原语，MMT允许我们整合现有的表示语言的正式数学知识在一个简单的，可扩展的形式主义。特别是，MMT从底层的数学和逻辑基础中抽象出来，以便它可以作为正式数字图书馆的标准化表示格式。此外，MMT系统地分离逻辑相关和逻辑无关的关注点，使它可以作为计算系统和MKM系统之间的接口层。
英文摘要：
Symbolic and logic computation systems ranging from computer algebra systems to theorem provers are finding their way into science, technology, mathematics and engineering. But such systems rely on explicitly or implicitly represented mathematical knowledge that needs to be managed to use such systems effectively. While mathematical knowledge management (MKM) "in the small" is well-studied, scaling up to large, highly interconnected corpora remains difficult. We hold that in order to realize MKM "in the large", we need representation languages and software architectures that are designed systematically with large-scale processing in mind. Therefore, we have designed and implemented the MMT language -- a module system for mathematical theories. MMT is designed as the simplest possible language that combines a module system, a foundationally uncommitted formal semantics, and web-scalable implementations. Due to a careful choice of representational primitives, MMT allows us to integrate existing representation languages for formal mathematical knowledge in a simple, scalable formalism. In particular, MMT abstracts from the underlying mathematical and logical foundations so that it can serve as a standardized representation format for a formal digital library. Moreover, MMT systematically separates logic-dependent and logic-independent concerns so that it can serve as an interface layer between computation systems and MKM systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
