形式数学库的一种查询语言
A Query Language for Formal Mathematical Libraries
摘要：
数学知识管理最有前途的应用之一是搜索：即使我们将注意力限制在已经形式化的数学的微小片段上，其数量也超过了个人的理解力。基于通用表示语言MMT，我们介绍了数学查询语言QMT：它结合了简单性，表达性和可扩展性，同时避免了一个特定的逻辑形式主义的承诺。QMT可以集成各种搜索范式，如统一，语义网，或XQuery风格的查询，QMT查询可以跨越不同的数学库。我们已经实现了QMT作为MMT API的一部分。这种组合提供了一个可伸缩的索引和查询引擎，可以很容易地应用于任何数学知识库。虽然我们这里的重点是在内容标记语言中可用的库，但QMT自然会扩展到表示和叙述置标语言。
英文摘要：
One of the most promising applications of mathematical knowledge management is search: Even if we restrict attention to the tiny fragment of mathematics that has been formalized, the amount exceeds the comprehension of an individual human. Based on the generic representation language MMT, we introduce the mathematical query language QMT: It combines simplicity, expressivity, and scalability while avoiding a commitment to a particular logical formalism. QMT can integrate various search paradigms such as unification, semantic web, or XQuery style queries, and QMT queries can span different mathematical libraries. We have implemented QMT as a part of the MMT API. This combination provides a scalable indexing and query engine that can be readily applied to any library of mathematical knowledge. While our focus here is on libraries that are available in a content markup language, QMT naturally extends to presentation and narration markup languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
